1 /-
2 Copyright (c) 2018 Johannes Hölzl. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Johannes Hölzl, Jens Wagemaker
5
6 GCD domain and integral domains with normalization functions
7
8 TODO: abstract the domains to to semi domains (i.e. domains on semirings) to include ℕ and ℕ[X] etc.
9 -/
10 import algebra.associated data.int.gcd
src └────────────────┘ └──────────┘
11
12 variables {α : Type*}
13
14 set_option old_structure_cmd true
doc └───────────────┘
15
16
17
18 section prio
19 set_option default_priority 100 -- see Note [default priority]
doc └──────────────┘
20 /-- Normalization domain: multiplying with `norm_unit` gives a normal form for associated elements. -/
21 class normalization_domain (α : Type*) extends integral_domain α :=
id ┴ └───┘ └─────────────┘ ┴
src └─────────────┘
typ ┴ └───┘ └─────────────┘ ┴
22 (norm_unit : α → units α)
id ┴ ┴ └───┘ ┴
src └───┘
typ ┴ ┴ └───┘ ┴
23 (norm_unit_zero : norm_unit 0 = 1)
id └───────┘ ┴
src ┴
typ └───────┘ ┴
24 (norm_unit_mul : ∀{a b}, a ≠ 0 → b ≠ 0 → norm_unit (a * b) = norm_unit a * norm_unit b)
id ┴┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
src ┴ ┴ ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
25 (norm_unit_coe_units : ∀(u : units α), norm_unit u = u⁻¹)
id ┴ └───┘ ┴ └───────┘ ┴ ┴ ┴└┘
src └───┘ ┴ └┘
typ ┴ └───┘ ┴ └───────┘ ┴ ┴ ┴└┘
26 end prio
27
28 export normalization_domain (norm_unit norm_unit_zero norm_unit_mul norm_unit_coe_units)
29
30 attribute [simp] norm_unit_coe_units norm_unit_zero norm_unit_mul
id └─────────────────┘ └────────────┘ └───────────┘
src └─────────────────┘ └────────────┘ └───────────┘
typ └─────────────────┘ └────────────┘ └───────────┘
doc └──┘
31
32 section normalization_domain
33 variable [normalization_domain α]
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
34
35 def normalize (x : α) : α :=
id ┴ ┴
typ ┴ ┴
36 x * norm_unit x
id ┴ ┴ └───────┘ ┴
src ┴ └───────┘
typ ┴ ┴ └───────┘ ┴
37
38 theorem associated_normalize {x : α} : associated x (normalize x) :=
id ┴ └────────┘ ┴ └───────┘ ┴
src └────────┘ └───────┘
typ ┴ └────────┘ ┴ └───────┘ ┴
39 ⟨_, rfl⟩
id └─┘
src └─┘
typ └─┘
40
41 theorem normalize_associated {x : α} : associated (normalize x) x :=
id ┴ └────────┘ └───────┘ ┴ ┴
src └────────┘ └───────┘
typ ┴ └────────┘ └───────┘ ┴ ┴
42 associated_normalize.symm
id └──────────────────┘└───┘
src └──────────────────┘└───┘
typ └──────────────────┘└───┘
43
44 @[simp] theorem norm_unit_one : norm_unit (1:α) = 1 :=
id └───────┘ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴
doc └──┘
45 norm_unit_coe_units 1
id └─────────────────┘
src └─────────────────┘
typ └─────────────────┘
46
47 @[simp] lemma normalize_zero : normalize (0 : α) = 0 :=
id └───────┘ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴
doc └──┘
48 by rw [normalize, zero_mul]
id └───────┘ └──────┘
src └──┘└───────┘└┘└──────┘└─
typ └──┘└───────┘└┘└──────┘└─
doc └──┘ └┘ └─
txt └──┘ └┘ └─
par └──┘ └┘ └─
pid └┘ └┘ ┴└
st └────────────┘└────────┘┴└
49
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
50 @[simp] lemma normalize_one : normalize (1 : α) = 1 :=
id └───────┘ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴
doc └──┘
51 by rw [normalize, norm_unit_one, units.coe_one, mul_one]
id └───────┘ └───────────┘ └───────────┘ └─────┘
src └──┘└───────┘└┘└───────────┘└┘└───────────┘└┘└─────┘└─
typ └──┘└───────┘└┘└───────────┘└┘└───────────┘└┘└─────┘└─
doc └──┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ ┴└
st └────────────┘└─────────────┘└─────────────┘└───────┘┴└
52
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
53 lemma normalize_coe_units (u : units α) : normalize (u : α) = 1 :=
id └───┘ ┴ └───────┘ ┴ ┴ ┴
src └───┘ └───────┘ ┴
typ └───┘ ┴ └───────┘ ┴ ┴ ┴
54 by rw [normalize, norm_unit_coe_units, ← units.coe_mul, mul_inv_self, units.coe_one]
id └───────┘ └─────────────────┘ └───────────┘ └──────────┘ └───────────┘
src └──┘└───────┘└┘└─────────────────┘└──┘└───────────┘└┘└──────────┘└┘└───────────┘└─
typ └──┘└───────┘└┘└─────────────────┘└──┘└───────────┘└┘└──────────┘└┘└───────────┘└─
doc └──┘ └┘ └──┘ └┘ └┘ └─
txt └──┘ └┘ └──┘ └┘ └┘ └─
par └──┘ └┘ └──┘ └┘ └┘ └─
pid └┘ └┘ └──┘ └┘ └┘ ┴└
st └────────────┘└───────────────────┘└───────────────┘└────────────┘└─────────────┘┴└
55
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
56 theorem normalize_mul (x y : α) : normalize (x * y) = normalize x * normalize y :=
id ┴ └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
src └───────┘ ┴ ┴ └───────┘ ┴ └───────┘
typ ┴ └───────┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
57 classical.by_cases (λ hx : x = 0, by rw [hx, zero_mul, normalize_zero, zero_mul]) $ λ hx,
id └────────────────┘ ┴ ┴ └┘ └──────┘ └────────────┘ └──────┘ └┘
src └────────────────┘ ┴ └──┘ └┘└──────┘└┘└────────────┘└┘└──────┘┴
typ └────────────────┘ ┴ ┴ └──┘└┘└┘└──────┘└┘└────────────┘└┘└──────┘┴ └┘
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st └─────┘└────────┘└──────────────┘└────────┘┴
58 classical.by_cases (λ hy : y = 0, by rw [hy, mul_zero, normalize_zero, mul_zero]) $ λ hy,
id └────────────────┘ ┴ ┴ └┘ └──────┘ └────────────┘ └──────┘ └┘
src └────────────────┘ ┴ └──┘ └┘└──────┘└┘└────────────┘└┘└──────┘┴
typ └────────────────┘ ┴ ┴ └──┘└┘└┘└──────┘└┘└────────────┘└┘└──────┘┴ └┘
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st └─────┘└────────┘└──────────────┘└────────┘┴
59 by simp only [normalize, norm_unit_mul hx hy, units.coe_mul]; simp only [mul_assoc, mul_left_comm y]
id └───────┘ └───────────┘ └┘ └┘ └───────────┘ └───────┘ └───────────┘ ┴
src └─────────┘└───────┘└┘└───────────┘┴ ┴ └┘└───────────┘┴ └─────────┘└───────┘└┘└───────────┘┴ └─
typ └─────────┘└───────┘└┘└───────────┘┴└┘┴└┘└┘└───────────┘┴ └─────────┘└───────┘└┘└───────────┘┴┴└─
doc └─────────┘ └┘ ┴ ┴ └┘ ┴ └─────────┘ └┘ ┴ └─
txt └─────────┘ └┘ ┴ ┴ └┘ ┴ └─────────┘ └┘ ┴ └─
par └─────────┘ └┘ ┴ ┴ └┘ ┴ └─────────┘ └┘ ┴ └─
pid ┴└──┘└┘ └┘ ┴ ┴ └┘ ┴ ┴└──┘└┘ └┘ ┴ ┴└
st └──────────────────────────────────────────────────────────────────────────────────────────────────
60
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
61 lemma normalize_eq_zero {x : α} : normalize x = 0 ↔ x = 0 :=
id ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴
typ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
62 ⟨λ hx, (associated_zero_iff_eq_zero x).1 $ hx ▸ associated_normalize, by rintro rfl; exact normalize_zero⟩
id └┘ └─────────────────────────┘ ┴ ┴ └┘ ┴ └──────────────────┘ └────────────┘
src └─────────────────────────┘ ┴ ┴ └──────────────────┘ └────────┘ └────┘└────────────┘
typ └┘ └─────────────────────────┘ ┴ ┴ └┘ ┴ └──────────────────┘ └────────┘ └────┘└────────────┘
doc └────────┘ └────┘
txt └────────┘ └────┘
par └────────┘ └────┘
pid └──┘ ┴
st └───────────────────────────────┘
63
64 lemma normalize_eq_one {x : α} : normalize x = 1 ↔ is_unit x :=
id ┴ └───────┘ ┴ ┴ ┴ └─────┘ ┴
src └───────┘ ┴ ┴ └─────┘
typ ┴ └───────┘ ┴ ┴ ┴ └─────┘ ┴
doc └─────┘
65 ⟨λ hx, is_unit_iff_exists_inv.2 ⟨_, hx⟩, λ ⟨u, hu⟩, hu.symm ▸ normalize_coe_units u⟩
id └┘ └────────────────────┘┴ └┘ ┴┴ └┘ └───┘ ┴ └─────────────────┘
src └────────────────────┘┴ └───┘ ┴ └─────────────────┘
typ └┘ └────────────────────┘┴ └┘ ┴┴ └┘ └───┘ ┴ └─────────────────┘
66
67 theorem norm_unit_mul_norm_unit (a : α) : norm_unit (a * norm_unit a) = 1 :=
id ┴ └───────┘ ┴ ┴ └───────┘ ┴ ┴
src └───────┘ ┴ └───────┘ ┴
typ ┴ └───────┘ ┴ ┴ └───────┘ ┴ ┴
68 classical.by_cases (assume : a = 0, by simp only [this, norm_unit_zero, zero_mul]) $
id └────────────────┘ ┴ ┴ └──┘ └────────────┘ └──────┘
src └────────────────┘ ┴ └─────────┘ └┘└────────────┘└┘└──────┘┴
typ └────────────────┘ ┴ ┴ └─────────┘└──┘└┘└────────────┘└┘└──────┘┴
doc └─────────┘ └┘ └┘ ┴
txt └─────────┘ └┘ └┘ ┴
par └─────────┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴
st └─────────────────────────────────────────┘
69 assume h, by rw [norm_unit_mul h (units.ne_zero _), norm_unit_coe_units, mul_inv_eq_one]
id ┴ └───────────┘ ┴ └───────────┘ └─────────────────┘ └────────────┘
src └──┘└───────────┘┴ ┴ └───────────┘└───┘└─────────────────┘└┘└────────────┘└─
typ ┴ └──┘└───────────┘┴┴┴ └───────────┘└───┘└─────────────────┘└┘└────────────┘└─
doc └──┘ ┴ ┴ └───────────┘└───┘ └┘ └─
txt └──┘ ┴ ┴ └───┘ └┘ └─
par └──┘ ┴ ┴ └───┘ └┘ └─
pid └┘ ┴ ┴ └───┘ └┘ ┴└
st └────────────────────────────────────┘└───────────────────┘└──────────────┘┴└
70
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
71 theorem normalize_idem (x : α) : normalize (normalize x) = normalize x :=
id ┴ └───────┘ └───────┘ ┴ ┴ └───────┘ ┴
src └───────┘ └───────┘ ┴ └───────┘
typ ┴ └───────┘ └───────┘ ┴ ┴ └───────┘ ┴
72 by rw [normalize, normalize, norm_unit_mul_norm_unit, units.coe_one, mul_one]
id └───────┘ └───────┘ └─────────────────────┘ └───────────┘ └─────┘
src └──┘└───────┘└┘└───────┘└┘└─────────────────────┘└┘└───────────┘└┘└─────┘└─
typ └──┘└───────┘└┘└───────┘└┘└─────────────────────┘└┘└───────────┘└┘└─────┘└─
doc └──┘ └┘ └┘ └┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ └┘ ┴└
st └────────────┘└─────────┘└───────────────────────┘└─────────────┘└───────┘┴└
73
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
74 theorem normalize_eq_normalize {a b : α}
id ┴
typ ┴
75 (hab : a ∣ b) (hba : b ∣ a) : normalize a = normalize b :=
id ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
src ┴ ┴ └───────┘ ┴ └───────┘
typ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └───────┘ ┴
76 begin
st └─────
77 rcases associated_of_dvd_dvd hab hba with ⟨u, rfl⟩,
id └───────────────────┘ └─┘ └─┘
src └─────┘└───────────────────┘┴ ┴ └────────────┘
typ └─────┘└───────────────────┘┴└─┘┴└─┘└────────────┘
doc └─────┘ ┴ ┴ └────────────┘
txt └─────┘ ┴ ┴ └────────────┘
par └─────┘ ┴ ┴ └────────────┘
pid ┴ ┴ ┴ └────────────┘
st ───────────────────────────────────────────────────┘└─
78 refine classical.by_cases (by rintro rfl; simp only [zero_mul]) (assume ha : a ≠ 0, _),
id └────────────────┘ └──────┘ ┴ ┴
src └─────┘└────────────────┘┴ ┴└────────┘└┘└─────────┘└──────┘┴└┘ └────┘ ┴┴└────┘
typ └─────┘└────────────────┘┴ ┴└────────┘└┘└─────────┘└──────┘┴└┘ └────┘┴┴┴└────┘
doc └─────┘ ┴ ┴└────────┘└┘└─────────┘ ┴└┘ └────┘ ┴ └────┘
txt └─────┘ ┴ ┴└────────┘└┘└─────────┘ ┴└┘ └────┘ ┴ └────┘
par └─────┘ ┴ ┴└────────┘└┘└─────────┘ ┴└┘ └────┘ ┴ └────┘
pid ┴ ┴ └──────────────────────┘ └─┘ └────┘ ┴ └────┘
st ──────────────────────────────┘└───────────────────────────────┘└──────────────────────┘└─
79 suffices : a * ↑(norm_unit a) = a * ↑u * ↑(norm_unit a) * ↑u⁻¹,
id ┴ ┴ ┴ └───────┘ ┴ ┴└┘
src └─────────┘ ┴┴┴┴ ┴ └┘┴┴ ┴ ┴ ┴ ┴ └───────┘┴ └┘ ┴ └┘
typ └─────────┘ ┴┴┴┴ ┴ └┘┴┴ ┴ ┴ ┴ ┴ └───────┘┴┴└┘ ┴ ┴└┘
doc └─────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
txt └─────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
par └─────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
pid └───────┘└┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ ┴
st ───────────────────────────────────────────────────────────────┘
80 by simpa only [normalize, mul_assoc, norm_unit_mul ha u.ne_zero, norm_unit_coe_units],
id └───────┘ └───────┘ └───────────┘ └┘ └───────┘ └─────────────────┘
src └──────────┘└───────┘└┘└───────┘└┘└───────────┘┴ ┴└───────┘└┘└─────────────────┘┴
typ └──────────┘└───────┘└┘└───────┘└┘└───────────┘┴└┘┴└───────┘└┘└─────────────────┘┴
doc └──────────┘ └┘ └┘ ┴ ┴└───────┘└┘ ┴
txt └──────────┘ └┘ └┘ ┴ ┴ └┘ ┴
par └──────────┘ └┘ └┘ ┴ ┴ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ ┴ ┴ └┘ ┴
st └─
81 calc a * ↑(norm_unit a) = a * ↑(norm_unit a) * ↑u * ↑u⁻¹:
id └──┘
src └──┘
typ └──┘
doc └──┘
st ────────────────────────────────────────────────────────────
82 (units.mul_inv_cancel_right _ _).symm
id └────────────────────────┘ └──┘
src └────────────────────────┘ └──┘
typ └────────────────────────┘ └──┘
st ────────────────────────────────────────────
83 ... = a * ↑u * ↑(norm_unit a) * ↑u⁻¹ : by rw mul_right_comm a
id └───────┘ ┴ ┴ └────────────┘ ┴
src └───────┘ └─┘└────────────┘┴ ┴
typ └───────┘ ┴ ┴ └─┘└────────────┘┴┴┴
doc └─┘ ┴ ┴
txt └─┘ ┴ ┴
par └─┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────────────────────────────────┘└───────────────────┘
84 end
st └─┘
85
86 lemma normalize_eq_normalize_iff {x y : α} : normalize x = normalize y ↔ x ∣ y ∧ y ∣ x :=
id ┴ └───────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ └───────┘ ┴ ┴ ┴ ┴
typ ┴ └───────┘ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
87 ⟨λ h, ⟨dvd_mul_unit_iff.1 ⟨_, h.symm⟩, dvd_mul_unit_iff.1 ⟨_, h⟩⟩,
id ┴ └──────────────┘┴ ┴└───┘ └──────────────┘┴ ┴
src └──────────────┘┴ └───┘ └──────────────┘┴
typ ┴ └──────────────┘┴ ┴└───┘ └──────────────┘┴ ┴
88 λ ⟨hxy, hyx⟩, normalize_eq_normalize hxy hyx⟩
id ┴└─┘ └─┘ └────────────────────┘
src └────────────────────┘
typ ┴└─┘ └─┘ └────────────────────┘
89
90 theorem dvd_antisymm_of_normalize_eq {a b : α}
id ┴
typ ┴
91 (ha : normalize a = a) (hb : normalize b = b) (hab : a ∣ b) (hba : b ∣ a) :
id └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ └───────┘ ┴ ┴ ┴
typ └───────┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
92 a = b :=
id ┴ ┴ ┴
src ┴
typ ┴ ┴ ┴
93 ha ▸ hb ▸ normalize_eq_normalize hab hba
id └┘ ┴ └┘ ┴ └────────────────────┘ └─┘ └─┘
src ┴ ┴ └────────────────────┘
typ └┘ ┴ └┘ ┴ └────────────────────┘ └─┘ └─┘
94
95 @[simp] lemma dvd_normalize_iff {a b : α} : a ∣ normalize b ↔ a ∣ b :=
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
src ┴ └───────┘ ┴ ┴
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴
doc └──┘
96 dvd_mul_unit_iff
id └──────────────┘
src └──────────────┘
typ └──────────────┘
97
98 @[simp] lemma normalize_dvd_iff {a b : α} : normalize a ∣ b ↔ a ∣ b :=
id ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴ ┴
typ ┴ └───────┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
99 mul_unit_dvd_iff
id └──────────────┘
src └──────────────┘
typ └──────────────┘
100
101 end normalization_domain
102
103 namespace associates
104 variable [normalization_domain α]
id └──────────────────┘
src └──────────────────┘
typ └──────────────────┘
doc └──────────────────┘
105
106 local attribute [instance] associated.setoid
id └───────────────┘
src └───────────────┘
typ └───────────────┘
107
108 protected def out : associates α → α :=
id └────────┘ ┴ ┴
src └────────┘
typ └────────┘ ┴ ┴
109 quotient.lift (normalize : α → α) $ λ a b ⟨u, hu⟩, hu ▸
id └───────────┘ └───────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
src └───────────┘ └───────┘ ┴
typ └───────────┘ └───────┘ ┴ ┴ ┴ ┴ ┴ └┘ ┴
110 normalize_eq_normalize ⟨_, rfl⟩ (mul_unit_dvd_iff.2 $ dvd_refl a)
id └────────────────────┘ └─┘ └──────────────┘┴ └──────┘ ┴
src └────────────────────┘ └─┘ └──────────────┘┴ └──────┘
typ └────────────────────┘ └─┘ └──────────────┘┴ └──────┘ ┴
111
112 lemma out_mk (a : α) : (associates.mk a).out = normalize a := rfl
id ┴ └───────────┘ ┴ └─┘ ┴ └───────┘ ┴ └─┘
src └───────────┘ └─┘ ┴ └───────┘ └─┘
typ ┴ └───────────┘ ┴ └─┘ ┴ └───────┘ ┴ └─┘
113
114 @[simp] lemma out_one : (1 : associates α).out = 1 :=
id └────────┘ ┴ └─┘ ┴
src └────────┘ └─┘ ┴
typ └────────┘ ┴ └─┘ ┴
doc └──┘
115 normalize_one
id └───────────┘
src └───────────┘
typ └───────────┘
116
117 lemma out_mul (a b : associates α) : (a * b).out = a.out * b.out :=
id └────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└──┘
src └────────┘ ┴ └─┘ ┴ └──┘ ┴ └──┘
typ └────────┘ ┴ ┴ ┴ ┴ └─┘ ┴ ┴└──┘ ┴ ┴└──┘
118 quotient.induction_on₂ a b $ assume a b,
id └────────────────────┘ ┴ ┴ ┴ ┴
src └────────────────────┘
typ └────────────────────┘ ┴ ┴ ┴ ┴
119 by simp only [associates.quotient_mk_eq_mk, out_mk, mk_mul_mk, normalize_mul]
id └──────────────────────────┘ └────┘ └───────┘ └───────────┘
src └─────────┘└──────────────────────────┘└┘└────┘└┘└───────┘└┘└───────────┘└─
typ └─────────┘└──────────────────────────┘└┘└────┘└┘└───────┘└┘└───────────┘└─
doc └─────────┘ └┘ └┘ └┘ └─
txt └─────────┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ ┴└
st └───────────────────────────────────────────────────────────────────────────
120
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
121 lemma dvd_out_iff (a : α) (b : associates α) : a ∣ b.out ↔ associates.mk a ≤ b :=
id ┴ └────────┘ ┴ ┴ ┴ ┴└──┘ ┴ └───────────┘ ┴ ┴ ┴
src └────────┘ ┴ └──┘ ┴ └───────────┘ ┴
typ ┴ └────────┘ ┴ ┴ ┴ ┴└──┘ ┴ └───────────┘ ┴ ┴ ┴
122 quotient.induction_on b $ by simp [associates.out_mk, associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd_iff]
id └───────────────────┘ ┴ └───────────────┘ └──────────────────────────┘ └──────────────────┘
src └───────────────────┘ └────┘└───────────────┘└┘└──────────────────────────┘└┘└──────────────────┘└─
typ └───────────────────┘ ┴ └────┘└───────────────┘└┘└──────────────────────────┘└┘└──────────────────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └─────────────────────────────────────────────────────────────────────────────
123
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
124 lemma out_dvd_iff (a : α) (b : associates α) : b.out ∣ a ↔ b ≤ associates.mk a :=
id ┴ └────────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴
src └────────┘ └──┘ ┴ ┴ ┴ └───────────┘
typ ┴ └────────┘ ┴ ┴└──┘ ┴ ┴ ┴ ┴ ┴ └───────────┘ ┴
125 quotient.induction_on b $ by simp [associates.out_mk, associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd_iff]
id └───────────────────┘ ┴ └───────────────┘ └──────────────────────────┘ └──────────────────┘
src └───────────────────┘ └────┘└───────────────┘└┘└──────────────────────────┘└┘└──────────────────┘└─
typ └───────────────────┘ ┴ └────┘└───────────────┘└┘└──────────────────────────┘└┘└──────────────────┘└─
doc └────┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └─
par └────┘ └┘ └┘ └─
pid ┴┴ └┘ └┘ ┴└
st └─────────────────────────────────────────────────────────────────────────────
126
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
127 @[simp] lemma out_top : (⊤ : associates α).out = 0 :=
id ┴ └────────┘ ┴ └─┘ ┴
src ┴ └────────┘ └─┘ ┴
typ ┴ └────────┘ ┴ └─┘ ┴
doc └──┘
128 normalize_zero
id └────────────┘
src └────────────┘
typ └────────────┘
129
130 @[simp] lemma normalize_out (a : associates α) : normalize a.out = a.out :=
id └────────┘ ┴ └───────┘ ┴└──┘ ┴ ┴└──┘
src └────────┘ └───────┘ └──┘ ┴ └──┘
typ └────────┘ ┴ └───────┘ ┴└──┘ ┴ ┴└──┘
doc └──┘
131 quotient.induction_on a normalize_idem
id └───────────────────┘ ┴ └────────────┘
src └───────────────────┘ └────────────┘
typ └───────────────────┘ ┴ └────────────┘
132
133 end associates
134
135 section prio
136 set_option default_priority 100 -- see Note [default priority]
doc └──────────────┘
137 /-- GCD domain: an integral domain with normalization and `gcd` (greatest common divisor) and
138 `lcm` (least common multiple) operations. In this setting `gcd` and `lcm` form a bounded lattice on
139 the associated elements where `gcd` is the infimum, `lcm` is the supremum, `1` is bottom, and
140 `0` is top. The type class focuses on `gcd` and we derive the correpsonding `lcm` facts from `gcd`.
141 -/
142 class gcd_domain (α : Type*) extends normalization_domain α :=
id ┴ └───┘ └──────────────────┘ ┴
src └──────────────────┘
typ ┴ └───┘ └──────────────────┘ ┴
doc └──────────────────┘
143 (gcd : α → α → α)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
144 (lcm : α → α → α)
id ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
145 (gcd_dvd_left : ∀a b, gcd a b ∣ a)
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
146 (gcd_dvd_right : ∀a b, gcd a b ∣ b)
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
147 (dvd_gcd : ∀{a b c}, a ∣ c → a ∣ b → a ∣ gcd c b)
id ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴
typ ┴┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
148 (normalize_gcd : ∀a b, normalize (gcd a b) = gcd a b)
id ┴ ┴ └───────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └───────┘ ┴
typ ┴ ┴ └───────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
149 (gcd_mul_lcm : ∀a b, gcd a b * lcm a b = normalize (a * b))
id ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
src ┴ ┴ └───────┘ ┴
typ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
150 (lcm_zero_left : ∀a, lcm 0 a = 0)
id ┴ └─┘ ┴ ┴
src ┴
typ ┴ └─┘ ┴ ┴
151 (lcm_zero_right : ∀a, lcm a 0 = 0)
id ┴ └─┘ ┴ ┴
src ┴
typ ┴ └─┘ ┴ ┴
152 end prio
153
154 export gcd_domain (gcd lcm gcd_dvd_left gcd_dvd_right dvd_gcd lcm_zero_left lcm_zero_right)
155
156 attribute [simp] lcm_zero_left lcm_zero_right
id └───────────┘ └────────────┘
src └───────────┘ └────────────┘
typ └───────────┘ └────────────┘
doc └──┘
157
158 section gcd_domain
159 variables [gcd_domain α]
id └────────┘
src └────────┘
typ └────────┘
doc └────────┘
160
161 @[simp] theorem normalize_gcd : ∀a b:α, normalize (gcd a b) = gcd a b :=
id ┴ └───────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └───────┘ └─┘ ┴ └─┘
typ ┴ └───────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
doc └──┘
162 gcd_domain.normalize_gcd
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
163
164 @[simp] theorem gcd_mul_lcm : ∀a b:α, gcd a b * lcm a b = normalize (a * b) :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴ └───────┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
doc └──┘
165 gcd_domain.gcd_mul_lcm
id └────────────────────┘
src └────────────────────┘
typ └────────────────────┘
166
167 section gcd
168
169 theorem dvd_gcd_iff (a b c : α) : a ∣ gcd b c ↔ (a ∣ b ∧ a ∣ c) :=
id ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
170 iff.intro
id └───────┘
src └───────┘
typ └───────┘
171 (assume h, ⟨dvd_trans h (gcd_dvd_left _ _), dvd_trans h (gcd_dvd_right _ _)⟩)
id ┴ └───────┘ ┴ └──────────┘ └───────┘ ┴ └───────────┘
src └───────┘ └──────────┘ └───────┘ └───────────┘
typ ┴ └───────┘ ┴ └──────────┘ └───────┘ ┴ └───────────┘
172 (assume ⟨hab, hac⟩, dvd_gcd hab hac)
id ┴└─┘ └─┘ └─────┘
src └─────┘
typ ┴└─┘ └─┘ └─────┘
173
174 theorem gcd_comm (a b : α) : gcd a b = gcd b a :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └─┘ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
175 dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)
id └──────────────────────────┘ └───────────┘ └───────────┘
src └──────────────────────────┘ └───────────┘ └───────────┘
typ └──────────────────────────┘ └───────────┘ └───────────┘
176 (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))
id └─────┘ └───────────┘ └──────────┘
src └─────┘ └───────────┘ └──────────┘
typ └─────┘ └───────────┘ └──────────┘
177 (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))
id └─────┘ └───────────┘ └──────────┘
src └─────┘ └───────────┘ └──────────┘
typ └─────┘ └───────────┘ └──────────┘
178
179 theorem gcd_assoc (m n k : α) : gcd (gcd m n) k = gcd m (gcd n k) :=
id ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
src └─┘ └─┘ ┴ └─┘ └─┘
typ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
180 dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)
id └──────────────────────────┘ └───────────┘ └───────────┘
src └──────────────────────────┘ └───────────┘ └───────────┘
typ └──────────────────────────┘ └───────────┘ └───────────┘
181 (dvd_gcd
id └─────┘
src └─────┘
typ └─────┘
182 (dvd.trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_left m n))
id └───────┘ └──────────┘ └─┘ ┴ ┴ ┴ └──────────┘ ┴ ┴
src └───────┘ └──────────┘ └─┘ └──────────┘
typ └───────┘ └──────────┘ └─┘ ┴ ┴ ┴ └──────────┘ ┴ ┴
183 (dvd_gcd (dvd.trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_right m n)) (gcd_dvd_right (gcd m n) k)))
id └─────┘ └───────┘ └──────────┘ └─┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ └─┘ ┴ ┴ ┴
src └─────┘ └───────┘ └──────────┘ └─┘ └───────────┘ └───────────┘ └─┘
typ └─────┘ └───────┘ └──────────┘ └─┘ ┴ ┴ ┴ └───────────┘ ┴ ┴ └───────────┘ └─┘ ┴ ┴ ┴
184 (dvd_gcd
id └─────┘
src └─────┘
typ └─────┘
185 (dvd_gcd (gcd_dvd_left m (gcd n k)) (dvd.trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_left n k)))
id └─────┘ └──────────┘ ┴ └─┘ ┴ ┴ └───────┘ └───────────┘ ┴ └─┘ ┴ ┴ └──────────┘ ┴ ┴
src └─────┘ └──────────┘ └─┘ └───────┘ └───────────┘ └─┘ └──────────┘
typ └─────┘ └──────────┘ ┴ └─┘ ┴ ┴ └───────┘ └───────────┘ ┴ └─┘ ┴ ┴ └──────────┘ ┴ ┴
186 (dvd.trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k)))
id └───────┘ └───────────┘ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
src └───────┘ └───────────┘ └─┘ └───────────┘
typ └───────┘ └───────────┘ ┴ └─┘ ┴ ┴ └───────────┘ ┴ ┴
187
188 instance : is_commutative α gcd := ⟨gcd_comm⟩
id └────────────┘ ┴ └─┘ └──────┘
src └────────────┘ └─┘ └──────┘
typ └────────────┘ ┴ └─┘ └──────┘
189 instance : is_associative α gcd := ⟨gcd_assoc⟩
id └────────────┘ ┴ └─┘ └───────┘
src └────────────┘ └─┘ └───────┘
typ └────────────┘ ┴ └─┘ └───────┘
190
191 theorem gcd_eq_normalize {a b c : α} (habc : gcd a b ∣ c) (hcab : c ∣ gcd a b) :
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src └─┘ ┴ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
192 gcd a b = normalize c :=
id └─┘ ┴ ┴ ┴ └───────┘ ┴
src └─┘ ┴ └───────┘
typ └─┘ ┴ ┴ ┴ └───────┘ ┴
193 normalize_gcd a b ▸ normalize_eq_normalize habc hcab
id └───────────┘ ┴ ┴ ┴ └────────────────────┘ └──┘ └──┘
src └───────────┘ ┴ └────────────────────┘
typ └───────────┘ ┴ ┴ ┴ └────────────────────┘ └──┘ └──┘
194
195 @[simp] theorem gcd_zero_left (a : α) : gcd 0 a = normalize a :=
id ┴ └─┘ ┴ ┴ └───────┘ ┴
src └─┘ ┴ └───────┘
typ ┴ └─┘ ┴ ┴ └───────┘ ┴
doc └──┘
196 gcd_eq_normalize (gcd_dvd_right 0 a) (dvd_gcd (dvd_zero _) (dvd_refl a))
id └──────────────┘ └───────────┘ ┴ └─────┘ └──────┘ └──────┘ ┴
src └──────────────┘ └───────────┘ └─────┘ └──────┘ └──────┘
typ └──────────────┘ └───────────┘ ┴ └─────┘ └──────┘ └──────┘ ┴
197
198 @[simp] theorem gcd_zero_right (a : α) : gcd a 0 = normalize a :=
id ┴ └─┘ ┴ ┴ └───────┘ ┴
src └─┘ ┴ └───────┘
typ ┴ └─┘ ┴ ┴ └───────┘ ┴
doc └──┘
199 gcd_eq_normalize (gcd_dvd_left a 0) (dvd_gcd (dvd_refl a) (dvd_zero _))
id └──────────────┘ └──────────┘ ┴ └─────┘ └──────┘ ┴ └──────┘
src └──────────────┘ └──────────┘ └─────┘ └──────┘ └──────┘
typ └──────────────┘ └──────────┘ ┴ └─────┘ └──────┘ ┴ └──────┘
200
201 @[simp] theorem gcd_eq_zero_iff (a b : α) : gcd a b = 0 ↔ a = 0 ∧ b = 0 :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
202 iff.intro
id └───────┘
src └───────┘
typ └───────┘
203 (assume h, let ⟨ca, ha⟩ := gcd_dvd_left a b, ⟨cb, hb⟩ := gcd_dvd_right a b in
id ┴ └─┘ └──────────┘ ┴ ┴ └───────────┘ ┴ ┴
src └──────────┘ └───────────┘
typ ┴ └─┘ └──────────┘ ┴ ┴ └───────────┘ ┴ ┴
204 by rw [h, zero_mul] at ha hb; exact ⟨ha, hb⟩)
id ┴ └──────┘ └┘ └┘
src └──┘ └┘└──────┘└────────┘ └────┘ └┘ ┴
typ └──┘┴└┘└──────┘└────────┘ └────┘ └┘└┘└┘┴
doc └──┘ └┘ └────────┘ └────┘ └┘ ┴
txt └──┘ └┘ └────────┘ └────┘ └┘ ┴
par └──┘ └┘ └────────┘ └────┘ └┘ ┴
pid └┘ └┘ ┴└───────┘ ┴ └┘ ┴
st └────┘└────────┘┴└───────────────────────┘
205 (assume ⟨ha, hb⟩, by rw [ha, hb, gcd_zero_left, normalize_zero])
id ┴ └┘ └┘ └───────────┘ └────────────┘
src └──┘ └┘ └┘└───────────┘└┘└────────────┘┴
typ ┴ └──┘└┘└┘└┘└┘└───────────┘└┘└────────────┘┴
doc └──┘ └┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ └┘ ┴
par └──┘ └┘ └┘ └┘ ┴
pid └┘ └┘ └┘ └┘ ┴
st └─────┘└──┘└─────────────┘└──────────────┘┴
206
207 @[simp] theorem gcd_one_left (a : α) : gcd 1 a = 1 :=
id ┴ └─┘ ┴ ┴
src └─┘ ┴
typ ┴ └─┘ ┴ ┴
doc └──┘
208 dvd_antisymm_of_normalize_eq (normalize_gcd _ _) normalize_one (gcd_dvd_left _ _) (one_dvd _)
id └──────────────────────────┘ └───────────┘ └───────────┘ └──────────┘ └─────┘
src └──────────────────────────┘ └───────────┘ └───────────┘ └──────────┘ └─────┘
typ └──────────────────────────┘ └───────────┘ └───────────┘ └──────────┘ └─────┘
209
210 @[simp] theorem gcd_one_right (a : α) : gcd a 1 = 1 :=
id ┴ └─┘ ┴ ┴
src └─┘ ┴
typ ┴ └─┘ ┴ ┴
doc └──┘
211 dvd_antisymm_of_normalize_eq (normalize_gcd _ _) normalize_one (gcd_dvd_right _ _) (one_dvd _)
id └──────────────────────────┘ └───────────┘ └───────────┘ └───────────┘ └─────┘
src └──────────────────────────┘ └───────────┘ └───────────┘ └───────────┘ └─────┘
typ └──────────────────────────┘ └───────────┘ └───────────┘ └───────────┘ └─────┘
212
213 theorem gcd_dvd_gcd {a b c d: α} (hab : a ∣ b) (hcd : c ∣ d) : gcd a c ∣ gcd b d :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ ┴ └─┘ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
214 dvd_gcd (dvd.trans (gcd_dvd_left _ _) hab) (dvd.trans (gcd_dvd_right _ _) hcd)
id └─────┘ └───────┘ └──────────┘ └─┘ └───────┘ └───────────┘ └─┘
src └─────┘ └───────┘ └──────────┘ └───────┘ └───────────┘
typ └─────┘ └───────┘ └──────────┘ └─┘ └───────┘ └───────────┘ └─┘
215
216 @[simp] theorem gcd_same (a : α) : gcd a a = normalize a :=
id ┴ └─┘ ┴ ┴ ┴ └───────┘ ┴
src └─┘ ┴ └───────┘
typ ┴ └─┘ ┴ ┴ ┴ └───────┘ ┴
doc └──┘
217 gcd_eq_normalize (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) (dvd_refl a))
id └──────────────┘ └──────────┘ └─────┘ └──────┘ ┴ └──────┘ ┴
src └──────────────┘ └──────────┘ └─────┘ └──────┘ └──────┘
typ └──────────────┘ └──────────┘ └─────┘ └──────┘ ┴ └──────┘ ┴
218
219 @[simp] theorem gcd_mul_left (a b c : α) : gcd (a * b) (a * c) = normalize a * gcd b c :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ ┴ ┴ ┴ └───────┘ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ ┴
doc └──┘
220 classical.by_cases (by rintro rfl; simp only [zero_mul, gcd_zero_left, normalize_zero]) $ assume ha : a ≠ 0,
id └────────────────┘ └──────┘ └───────────┘ └────────────┘ ┴ ┴
src └────────────────┘ └────────┘ └─────────┘└──────┘└┘└───────────┘└┘└────────────┘┴ ┴
typ └────────────────┘ └────────┘ └─────────┘└──────┘└┘└───────────┘└┘└────────────┘┴ ┴ ┴
doc └────────┘ └─────────┘ └┘ └┘ ┴
txt └────────┘ └─────────┘ └┘ └┘ ┴
par └────────┘ └─────────┘ └┘ └┘ ┴
pid └──┘ ┴└──┘└┘ └┘ └┘ ┴
st └──────────────────────────────────────────────────────────────┘
221 suffices gcd (a * b) (a * c) = normalize (a * gcd b c),
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ ┴ ┴ ┴ └───────┘ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ ┴
222 by simpa only [normalize_mul, normalize_gcd],
id └───────────┘ └───────────┘
src └──────────┘└───────────┘└┘└───────────┘┴
typ └──────────┘└───────────┘└┘└───────────┘┴
doc └──────────┘ └┘ ┴
txt └──────────┘ └┘ ┴
par └──────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └────────────────────────────────────────┘
223 let ⟨d, eq⟩ := dvd_gcd (dvd_mul_right a b) (dvd_mul_right a c) in
id └─┘ ┴ └┘ └─────┘ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
src └┘ └─────┘ └───────────┘ └───────────┘
typ └─┘ ┴ └┘ └─────┘ └───────────┘ ┴ ┴ └───────────┘ ┴ ┴
224 gcd_eq_normalize
id └──────────────┘
src └──────────────┘
typ └──────────────┘
225 (eq.symm ▸ mul_dvd_mul_left a $ show d ∣ gcd b c, from
id └───┘ ┴ └──────────────┘ ┴ ┴ └─┘ ┴ ┴
src └───┘ ┴ └──────────────┘ ┴ └─┘
typ └───┘ ┴ └──────────────┘ ┴ ┴ └─┘ ┴ ┴
226 dvd_gcd
id └─────┘
src └─────┘
typ └─────┘
227 ((mul_dvd_mul_iff_left ha).1 $ eq ▸ gcd_dvd_left _ _)
id └──────────────────┘ └┘ ┴ ┴ └──────────┘
src └──────────────────┘ ┴ ┴ └──────────┘
typ └──────────────────┘ └┘ ┴ ┴ └──────────┘
doc └──────────────────┘
228 ((mul_dvd_mul_iff_left ha).1 $ eq ▸ gcd_dvd_right _ _))
id └──────────────────┘ └┘ ┴ ┴ └───────────┘
src └──────────────────┘ ┴ ┴ └───────────┘
typ └──────────────────┘ └┘ ┴ ┴ └───────────┘
doc └──────────────────┘
229 (dvd_gcd
id └─────┘
src └─────┘
typ └─────┘
230 (mul_dvd_mul_left a $ gcd_dvd_left _ _)
id └──────────────┘ ┴ └──────────┘
src └──────────────┘ └──────────┘
typ └──────────────┘ ┴ └──────────┘
231 (mul_dvd_mul_left a $ gcd_dvd_right _ _))
id └──────────────┘ ┴ └───────────┘
src └──────────────┘ └───────────┘
typ └──────────────┘ ┴ └───────────┘
232
233 @[simp] theorem gcd_mul_right (a b c : α) : gcd (b * a) (c * a) = gcd b c * normalize a :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───────┘ ┴
src └─┘ ┴ ┴ ┴ └─┘ ┴ └───────┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───────┘ ┴
doc └──┘
234 by simp only [mul_comm, gcd_mul_left]
id └──────┘ └──────────┘
src └─────────┘└──────┘└┘└──────────┘└─
typ └─────────┘└──────┘└┘└──────────┘└─
doc └─────────┘ └┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └───────────────────────────────────
235
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
236 theorem gcd_eq_left_iff (a b : α) (h : normalize a = a) : gcd a b = a ↔ a ∣ b :=
id ┴ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ └─┘ ┴ ┴ ┴
typ ┴ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
237 iff.intro (assume eq, eq ▸ gcd_dvd_right _ _) $
id └───────┘ └┘ └┘ ┴ └───────────┘
src └───────┘ └┘ └┘ ┴ └───────────┘
typ └───────┘ └┘ └┘ ┴ └───────────┘
238 assume hab, dvd_antisymm_of_normalize_eq (normalize_gcd _ _) h (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) hab)
id └─┘ └──────────────────────────┘ └───────────┘ ┴ └──────────┘ └─────┘ └──────┘ ┴ └─┘
src └──────────────────────────┘ └───────────┘ └──────────┘ └─────┘ └──────┘
typ └─┘ └──────────────────────────┘ └───────────┘ ┴ └──────────┘ └─────┘ └──────┘ ┴ └─┘
239
240 theorem gcd_eq_right_iff (a b : α) (h : normalize b = b) : gcd a b = b ↔ b ∣ a :=
id ┴ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ └─┘ ┴ ┴ ┴
typ ┴ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
241 by simpa only [gcd_comm a b] using gcd_eq_left_iff b a h
id └──────┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └──────────┘└──────┘┴ ┴ └──────┘└─────────────┘┴ ┴ ┴ └
typ └──────────┘└──────┘┴┴┴┴└──────┘└─────────────┘┴┴┴┴┴┴└
doc └──────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ └
txt └──────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ └
par └──────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ └
pid ┴└──┘└┘ ┴ ┴ ┴┴└────┘ ┴ ┴ ┴ └
st └──────────────────────────────────────────────────────
242
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
243 theorem gcd_dvd_gcd_mul_left (m n k : α) : gcd m n ∣ gcd (k * m) n :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
244 gcd_dvd_gcd (dvd_mul_left _ _) (dvd_refl _)
id └─────────┘ └──────────┘ └──────┘
src └─────────┘ └──────────┘ └──────┘
typ └─────────┘ └──────────┘ └──────┘
245
246 theorem gcd_dvd_gcd_mul_right (m n k : α) : gcd m n ∣ gcd (m * k) n :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
247 gcd_dvd_gcd (dvd_mul_right _ _) (dvd_refl _)
id └─────────┘ └───────────┘ └──────┘
src └─────────┘ └───────────┘ └──────┘
typ └─────────┘ └───────────┘ └──────┘
248
249 theorem gcd_dvd_gcd_mul_left_right (m n k : α) : gcd m n ∣ gcd m (k * n) :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
250 gcd_dvd_gcd (dvd_refl _) (dvd_mul_left _ _)
id └─────────┘ └──────┘ └──────────┘
src └─────────┘ └──────┘ └──────────┘
typ └─────────┘ └──────┘ └──────────┘
251
252 theorem gcd_dvd_gcd_mul_right_right (m n k : α) : gcd m n ∣ gcd m (n * k) :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
253 gcd_dvd_gcd (dvd_refl _) (dvd_mul_right _ _)
id └─────────┘ └──────┘ └───────────┘
src └─────────┘ └──────┘ └───────────┘
typ └─────────┘ └──────┘ └───────────┘
254
255 end gcd
256
257 section lcm
258
259 lemma lcm_dvd_iff {a b c : α} : lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
260 classical.by_cases
id └────────────────┘
src └────────────────┘
typ └────────────────┘
261 (assume : a = 0 ∨ b = 0, by rcases this with rfl | rfl;
id ┴ ┴ ┴ ┴ ┴ └──┘
src ┴ ┴ ┴ └─────┘ └─────────────┘
typ ┴ ┴ ┴ ┴ ┴ └─────┘└──┘└─────────────┘
doc └─────┘ └─────────────┘
txt └─────┘ └─────────────┘
par └─────┘ └─────────────┘
pid ┴ └─────────────┘
st └────────────────────────────
262 simp only [iff_def, lcm_zero_left, lcm_zero_right, zero_dvd_iff, dvd_zero,
id └─────┘ └───────────┘ └────────────┘ └──────────┘ └──────┘
src └─────────┘└─────┘└┘└───────────┘└┘└────────────┘└┘└──────────┘└┘└──────┘└─
typ └─────────┘└─────┘└┘└───────────┘└┘└────────────┘└┘└──────────┘└┘└──────┘└─
doc └─────────┘ └┘ └┘ └┘└──────────┘└┘ └─
txt └─────────┘ └┘ └┘ └┘ └┘ └─
par └─────────┘ └┘ └┘ └┘ └┘ └─
pid ┴└──┘└┘ └┘ └┘ └┘ └┘ └─
st ───────────────────────────────────────────────────────────────────────────────
263 eq_self_iff_true, and_true, imp_true_iff] {contextual:=tt})
id └──────────────┘ └──────┘ └──────────┘ └┘
src ─────┘└──────────────┘└┘└──────┘└┘└──────────┘└┘ └──────────┘└┘┴
typ ─────┘└──────────────┘└┘└──────┘└┘└──────────┘└┘ └──────────┘└┘┴
doc ─────┘ └┘ └┘ └┘ └──────────┘ ┴
txt ─────┘ └┘ └┘ └┘ └──────────┘ ┴
par ─────┘ └┘ └┘ └┘ └──────────┘ ┴
pid ─────┘ └┘ └┘ ┴┴ └──────────┘ ┴
st ───────────────────────────────────────────────────────────────┘
264 (assume this : ¬ (a = 0 ∨ b = 0),
id ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴
265 let ⟨h1, h2⟩ := not_or_distrib.1 this in
id └─┘ └┘ └────────────┘┴ └──┘
src └────────────┘┴
typ └─┘ └┘ └────────────┘┴ └──┘
266 have h : gcd a b ≠ 0, from λ H, h1 ((gcd_eq_zero_iff _ _).1 H).1,
id └─┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └─┘ ┴ └─────────────┘ ┴ ┴
typ └─┘ ┴ ┴ ┴ ┴ └─────────────┘ ┴ ┴ ┴
267 by rw [← mul_dvd_mul_iff_left h, gcd_mul_lcm, normalize_dvd_iff, ← dvd_normalize_iff,
id └──────────────────┘ ┴ └─────────┘ └───────────────┘ └───────────────┘
src └────┘└──────────────────┘┴ └┘└─────────┘└┘└───────────────┘└──┘└───────────────┘└─
typ └────┘└──────────────────┘┴┴└┘└─────────┘└┘└───────────────┘└──┘└───────────────┘└─
doc └────┘└──────────────────┘┴ └┘ └┘ └──┘ └─
txt └────┘ ┴ └┘ └┘ └──┘ └─
par └────┘ ┴ └┘ └┘ └──┘ └─
pid └──┘ ┴ └┘ └┘ └──┘ └─
st └───────────────────────────┘└───────────┘└─────────────────┘└───────────────────┘└─
268 normalize_mul, normalize_gcd, ← gcd_mul_right, dvd_gcd_iff,
id └───────────┘ └───────────┘ └───────────┘ └─────────┘
src ───────┘└───────────┘└┘└───────────┘└──┘└───────────┘└┘└─────────┘└─
typ ───────┘└───────────┘└┘└───────────┘└──┘└───────────┘└┘└─────────┘└─
doc ───────┘ └┘ └──┘ └┘ └─
txt ───────┘ └┘ └──┘ └┘ └─
par ───────┘ └┘ └──┘ └┘ └─
pid ───────┘ └┘ └──┘ └┘ └─
st ────────────────────┘└─────────────┘└───────────────┘└───────────┘└─
269 mul_comm b c, mul_dvd_mul_iff_left h1, mul_dvd_mul_iff_right h2, and_comm])
id └──────┘ ┴ ┴ └──────────────────┘ └┘ └───────────────────┘ └┘ └──────┘
src ───────┘└──────┘┴ ┴ └┘└──────────────────┘┴ └┘└───────────────────┘┴ └┘└──────┘┴
typ ───────┘└──────┘┴┴┴┴└┘└──────────────────┘┴└┘└┘└───────────────────┘┴└┘└┘└──────┘┴
doc ───────┘ ┴ ┴ └┘└──────────────────┘┴ └┘└───────────────────┘┴ └┘ ┴
txt ───────┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴
par ───────┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴
pid ───────┘ ┴ ┴ └┘ ┴ └┘ ┴ └┘ ┴
st ───────────────────┘└───────────────────────┘└────────────────────────┘└────────┘┴
270
271 lemma dvd_lcm_left (a b : α) : a ∣ lcm a b := (lcm_dvd_iff.1 (dvd_refl _)).1
id ┴ ┴ ┴ └─┘ ┴ ┴ └─────────┘┴ └──────┘ ┴
src ┴ └─┘ └─────────┘┴ └──────┘ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ └─────────┘┴ └──────┘ ┴
272
273 lemma dvd_lcm_right (a b : α) : b ∣ lcm a b := (lcm_dvd_iff.1 (dvd_refl _)).2
id ┴ ┴ ┴ └─┘ ┴ ┴ └─────────┘┴ └──────┘ ┴
src ┴ └─┘ └─────────┘┴ └──────┘ ┴
typ ┴ ┴ ┴ └─┘ ┴ ┴ └─────────┘┴ └──────┘ ┴
274
275 lemma lcm_dvd {a b c : α} (hab : a ∣ b) (hcb : c ∣ b) : lcm a c ∣ b :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ ┴ └─┘ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
276 lcm_dvd_iff.2 ⟨hab, hcb⟩
id └─────────┘┴ └─┘ └─┘
src └─────────┘┴
typ └─────────┘┴ └─┘ └─┘
277
278 @[simp] theorem lcm_eq_zero_iff (a b : α) : lcm a b = 0 ↔ a = 0 ∨ b = 0 :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
279 iff.intro
id └───────┘
src └───────┘
typ └───────┘
280 (assume h : lcm a b = 0,
id └─┘ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴
281 have normalize (a * b) = 0,
id └───────┘ ┴ ┴ ┴ ┴
src └───────┘ ┴ ┴
typ └───────┘ ┴ ┴ ┴ ┴
282 by rw [← gcd_mul_lcm _ _, h, mul_zero],
id └─────────┘ ┴ └──────┘
src └────┘└─────────┘└────┘ └┘└──────┘┴
typ └────┘└─────────┘└────┘┴└┘└──────┘┴
doc └────┘ └────┘ └┘ ┴
txt └────┘ └────┘ └┘ ┴
par └────┘ └────┘ └┘ ┴
pid └──┘ └────┘ └┘ ┴
st └────────────────────┘└─┘└────────┘┴
283 by simpa only [normalize_eq_zero, mul_eq_zero, units.ne_zero, or_false])
id └───────────────┘ └─────────┘ └───────────┘ └──────┘
src └──────────┘└───────────────┘└┘└─────────┘└┘└───────────┘└┘└──────┘┴
typ └──────────┘└───────────────┘└┘└─────────┘└┘└───────────┘└┘└──────┘┴
doc └──────────┘ └┘└─────────┘└┘└───────────┘└┘ ┴
txt └──────────┘ └┘ └┘ └┘ ┴
par └──────────┘ └┘ └┘ └┘ ┴
pid ┴└──┘└┘ └┘ └┘ └┘ ┴
st └───────────────────────────────────────────────────────────────────┘
284 (by rintro (rfl | rfl); [apply lcm_zero_left, apply lcm_zero_right])
id ┴ └───────────┘ └────────────┘
src └────────────────┘ ┴└────┘└───────────┘ └────┘└────────────┘
typ └────────────────┘ ┴└────┘└───────────┘ └────┘└────────────┘
doc └────────────────┘ └────┘ └────┘
txt └────────────────┘ └────┘ └────┘
par └────────────────┘ └────┘ └────┘
pid └──────────┘ ┴ ┴
st └──────────────────────────────────────────────────────────────┘
285
286 @[simp] lemma normalize_lcm (a b : α) : normalize (lcm a b) = lcm a b :=
id ┴ └───────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └───────┘ └─┘ ┴ └─┘
typ ┴ └───────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
doc └──┘
287 classical.by_cases (assume : lcm a b = 0, by rw [this, normalize_zero]) $
id └────────────────┘ └─┘ ┴ ┴ ┴ └──┘ └────────────┘
src └────────────────┘ └─┘ ┴ └──┘ └┘└────────────┘┴
typ └────────────────┘ └─┘ ┴ ┴ ┴ └──┘└──┘└┘└────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └───────┘└──────────────┘┴
288 assume h_lcm : lcm a b ≠ 0,
id └─┘ ┴ ┴ ┴
src └─┘ ┴
typ └─┘ ┴ ┴ ┴
289 have h1 : gcd a b ≠ 0, from mt (by rw [gcd_eq_zero_iff, lcm_eq_zero_iff];
id └─┘ ┴ ┴ ┴ └┘ └─────────────┘ └─────────────┘
src └─┘ ┴ └┘ └──┘└─────────────┘└┘└─────────────┘┴
typ └─┘ ┴ ┴ ┴ └┘ └──┘└─────────────┘└┘└─────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └──────────────────┘└───────────────┘┴└─
290 rintros ⟨rfl, rfl⟩; left; refl) h_lcm,
id └───┘
src └────────────────┘ └──┘ └──┘
typ └────────────────┘ └──┘ └──┘ └───┘
doc └────────────────┘ └──┘ └──┘
txt └────────────────┘ └──┘ └──┘
par └────────────────┘ └──┘ └──┘
pid └─────────┘
st ─────────────────────────────────┘
291 have h2 : normalize (gcd a b * lcm a b) = gcd a b * lcm a b,
id └───────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └───────┘ └─┘ ┴ └─┘ ┴ └─┘ ┴ └─┘
typ └───────┘ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
292 by rw [gcd_mul_lcm, normalize_idem],
id └─────────┘ └────────────┘
src └──┘└─────────┘└┘└────────────┘┴
typ └──┘└─────────┘└┘└────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └──────────────┘└──────────────┘┴
293 by simpa only [normalize_mul, normalize_gcd, one_mul, domain.mul_left_inj h1] using h2
id └───────────┘ └───────────┘ └─────┘ └─────────────────┘ └┘ └┘
src └──────────┘└───────────┘└┘└───────────┘└┘└─────┘└┘└─────────────────┘┴ └──────┘ └
typ └──────────┘└───────────┘└┘└───────────┘└┘└─────┘└┘└─────────────────┘┴└┘└──────┘└┘└
doc └──────────┘ └┘ └┘ └┘└─────────────────┘┴ └──────┘ └
txt └──────────┘ └┘ └┘ └┘ ┴ └──────┘ └
par └──────────┘ └┘ └┘ └┘ ┴ └──────┘ └
pid ┴└──┘└┘ └┘ └┘ └┘ ┴ ┴┴└────┘ └
st └────────────────────────────────────────────────────────────────────────────────────
294
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
295 theorem lcm_comm (a b : α) : lcm a b = lcm b a :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src └─┘ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
296 dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _)
id └──────────────────────────┘ └───────────┘ └───────────┘
src └──────────────────────────┘ └───────────┘ └───────────┘
typ └──────────────────────────┘ └───────────┘ └───────────┘
297 (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))
id └─────┘ └───────────┘ └──────────┘
src └─────┘ └───────────┘ └──────────┘
typ └─────┘ └───────────┘ └──────────┘
298 (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))
id └─────┘ └───────────┘ └──────────┘
src └─────┘ └───────────┘ └──────────┘
typ └─────┘ └───────────┘ └──────────┘
299
300 theorem lcm_assoc (m n k : α) : lcm (lcm m n) k = lcm m (lcm n k) :=
id ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
src └─┘ └─┘ ┴ └─┘ └─┘
typ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
301 dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _)
id └──────────────────────────┘ └───────────┘ └───────────┘
src └──────────────────────────┘ └───────────┘ └───────────┘
typ └──────────────────────────┘ └───────────┘ └───────────┘
302 (lcm_dvd
id └─────┘
src └─────┘
typ └─────┘
303 (lcm_dvd (dvd_lcm_left _ _) (dvd.trans (dvd_lcm_left _ _) (dvd_lcm_right _ _)))
id └─────┘ └──────────┘ └───────┘ └──────────┘ └───────────┘
src └─────┘ └──────────┘ └───────┘ └──────────┘ └───────────┘
typ └─────┘ └──────────┘ └───────┘ └──────────┘ └───────────┘
304 (dvd.trans (dvd_lcm_right _ _) (dvd_lcm_right _ _)))
id └───────┘ └───────────┘ └───────────┘
src └───────┘ └───────────┘ └───────────┘
typ └───────┘ └───────────┘ └───────────┘
305 (lcm_dvd
id └─────┘
src └─────┘
typ └─────┘
306 (dvd.trans (dvd_lcm_left _ _) (dvd_lcm_left _ _))
id └───────┘ └──────────┘ └──────────┘
src └───────┘ └──────────┘ └──────────┘
typ └───────┘ └──────────┘ └──────────┘
307 (lcm_dvd (dvd.trans (dvd_lcm_right _ _) (dvd_lcm_left _ _)) (dvd_lcm_right _ _)))
id └─────┘ └───────┘ └───────────┘ └──────────┘ └───────────┘
src └─────┘ └───────┘ └───────────┘ └──────────┘ └───────────┘
typ └─────┘ └───────┘ └───────────┘ └──────────┘ └───────────┘
308
309 instance : is_commutative α lcm := ⟨lcm_comm⟩
id └────────────┘ ┴ └─┘ └──────┘
src └────────────┘ └─┘ └──────┘
typ └────────────┘ ┴ └─┘ └──────┘
310 instance : is_associative α lcm := ⟨lcm_assoc⟩
id └────────────┘ ┴ └─┘ └───────┘
src └────────────┘ └─┘ └───────┘
typ └────────────┘ ┴ └─┘ └───────┘
311
312 lemma lcm_eq_normalize {a b c : α} (habc : lcm a b ∣ c) (hcab : c ∣ lcm a b) :
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src └─┘ ┴ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
313 lcm a b = normalize c :=
id └─┘ ┴ ┴ ┴ └───────┘ ┴
src └─┘ ┴ └───────┘
typ └─┘ ┴ ┴ ┴ └───────┘ ┴
314 normalize_lcm a b ▸ normalize_eq_normalize habc hcab
id └───────────┘ ┴ ┴ ┴ └────────────────────┘ └──┘ └──┘
src └───────────┘ ┴ └────────────────────┘
typ └───────────┘ ┴ ┴ ┴ └────────────────────┘ └──┘ └──┘
315
316 theorem lcm_dvd_lcm {a b c d : α} (hab : a ∣ b) (hcd : c ∣ d) : lcm a c ∣ lcm b d :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ ┴ └─┘ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
317 lcm_dvd (dvd.trans hab (dvd_lcm_left _ _)) (dvd.trans hcd (dvd_lcm_right _ _))
id └─────┘ └───────┘ └─┘ └──────────┘ └───────┘ └─┘ └───────────┘
src └─────┘ └───────┘ └──────────┘ └───────┘ └───────────┘
typ └─────┘ └───────┘ └─┘ └──────────┘ └───────┘ └─┘ └───────────┘
318
319 @[simp] theorem lcm_units_coe_left (u : units α) (a : α) : lcm ↑u a = normalize a :=
id └───┘ ┴ ┴ └─┘ ┴┴ ┴ ┴ └───────┘ ┴
src └───┘ └─┘ ┴ ┴ └───────┘
typ └───┘ ┴ ┴ └─┘ ┴┴ ┴ ┴ └───────┘ ┴
doc └──┘
320 lcm_eq_normalize (lcm_dvd (units.coe_dvd _ _) (dvd_refl _)) (dvd_lcm_right _ _)
id └──────────────┘ └─────┘ └───────────┘ └──────┘ └───────────┘
src └──────────────┘ └─────┘ └───────────┘ └──────┘ └───────────┘
typ └──────────────┘ └─────┘ └───────────┘ └──────┘ └───────────┘
doc └───────────┘
321
322 @[simp] theorem lcm_units_coe_right (a : α) (u : units α) : lcm a ↑u = normalize a :=
id ┴ └───┘ ┴ └─┘ ┴ ┴┴ ┴ └───────┘ ┴
src └───┘ └─┘ ┴ ┴ └───────┘
typ ┴ └───┘ ┴ └─┘ ┴ ┴┴ ┴ └───────┘ ┴
doc └──┘
323 (lcm_comm a u).trans $ lcm_units_coe_left _ _
id └──────┘ ┴ ┴ └───┘ └────────────────┘
src └──────┘ └───┘ └────────────────┘
typ └──────┘ ┴ ┴ └───┘ └────────────────┘
324
325 @[simp] theorem lcm_one_left (a : α) : lcm 1 a = normalize a :=
id ┴ └─┘ ┴ ┴ └───────┘ ┴
src └─┘ ┴ └───────┘
typ ┴ └─┘ ┴ ┴ └───────┘ ┴
doc └──┘
326 lcm_units_coe_left 1 a
id └────────────────┘ ┴
src └────────────────┘
typ └────────────────┘ ┴
327
328 @[simp] theorem lcm_one_right (a : α) : lcm a 1 = normalize a :=
id ┴ └─┘ ┴ ┴ └───────┘ ┴
src └─┘ ┴ └───────┘
typ ┴ └─┘ ┴ ┴ └───────┘ ┴
doc └──┘
329 lcm_units_coe_right a 1
id └─────────────────┘ ┴
src └─────────────────┘
typ └─────────────────┘ ┴
330
331 @[simp] theorem lcm_same (a : α) : lcm a a = normalize a :=
id ┴ └─┘ ┴ ┴ ┴ └───────┘ ┴
src └─┘ ┴ └───────┘
typ ┴ └─┘ ┴ ┴ ┴ └───────┘ ┴
doc └──┘
332 lcm_eq_normalize (lcm_dvd (dvd_refl _) (dvd_refl _)) (dvd_lcm_left _ _)
id └──────────────┘ └─────┘ └──────┘ └──────┘ └──────────┘
src └──────────────┘ └─────┘ └──────┘ └──────┘ └──────────┘
typ └──────────────┘ └─────┘ └──────┘ └──────┘ └──────────┘
333
334 @[simp] theorem lcm_eq_one_iff (a b : α) : lcm a b = 1 ↔ a ∣ 1 ∧ b ∣ 1 :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └─┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
doc └──┘
335 iff.intro
id └───────┘
src └───────┘
typ └───────┘
336 (assume eq, eq ▸ ⟨dvd_lcm_left _ _, dvd_lcm_right _ _⟩)
id └┘ └┘ ┴ └──────────┘ └───────────┘
src └┘ └┘ ┴ └──────────┘ └───────────┘
typ └┘ └┘ ┴ └──────────┘ └───────────┘
337 (assume ⟨⟨c, hc⟩, ⟨d, hd⟩⟩,
id ┴ ┴ └┘ ┴ └┘
typ ┴ ┴ └┘ ┴ └┘
338 show lcm (units.mk_of_mul_eq_one a c hc.symm : α) (units.mk_of_mul_eq_one b d hd.symm) = 1,
id └─┘ └────────────────────┘ ┴ └───┘ ┴ └────────────────────┘ ┴ └───┘ ┴
src └─┘ └────────────────────┘ └───┘ └────────────────────┘ └───┘ ┴
typ └─┘ └────────────────────┘ ┴ └───┘ ┴ └────────────────────┘ ┴ └───┘ ┴
339 by rw [lcm_units_coe_left, normalize_coe_units])
id └────────────────┘ └─────────────────┘
src └──┘└────────────────┘└┘└─────────────────┘┴
typ └──┘└────────────────┘└┘└─────────────────┘┴
doc └──┘ └┘ ┴
txt └──┘ └┘ ┴
par └──┘ └┘ ┴
pid └┘ └┘ ┴
st └─────────────────────┘└───────────────────┘┴
340
341 @[simp] theorem lcm_mul_left (a b c : α) : lcm (a * b) (a * c) = normalize a * lcm b c :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ ┴ ┴ ┴ └───────┘ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ ┴
doc └──┘
342 classical.by_cases (by rintro rfl; simp only [zero_mul, lcm_zero_left, normalize_zero]) $ assume ha : a ≠ 0,
id └────────────────┘ └──────┘ └───────────┘ └────────────┘ ┴ ┴
src └────────────────┘ └────────┘ └─────────┘└──────┘└┘└───────────┘└┘└────────────┘┴ ┴
typ └────────────────┘ └────────┘ └─────────┘└──────┘└┘└───────────┘└┘└────────────┘┴ ┴ ┴
doc └────────┘ └─────────┘ └┘ └┘ ┴
txt └────────┘ └─────────┘ └┘ └┘ ┴
par └────────┘ └─────────┘ └┘ └┘ ┴
pid └──┘ ┴└──┘└┘ └┘ └┘ ┴
st └──────────────────────────────────────────────────────────────┘
343 suffices lcm (a * b) (a * c) = normalize (a * lcm b c),
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ ┴
src └─┘ ┴ ┴ ┴ └───────┘ ┴ └─┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └─┘ ┴ ┴
344 by simpa only [normalize_mul, normalize_lcm],
id └───────────┘ └───────────┘
src └──────────┘└───────────┘└┘└───────────┘┴
typ └──────────┘└───────────┘└┘└───────────┘┴
doc └──────────┘ └┘ ┴
txt └──────────┘ └┘ ┴
par └──────────┘ └┘ ┴
pid ┴└──┘└┘ └┘ ┴
st └────────────────────────────────────────┘
345 have a ∣ lcm (a * b) (a * c), from dvd.trans (dvd_mul_right _ _) (dvd_lcm_left _ _),
id ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └───────────┘ └──────────┘
src ┴ └─┘ ┴ ┴ └───────┘ └───────────┘ └──────────┘
typ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ └───────┘ └───────────┘ └──────────┘
346 let ⟨d, eq⟩ := this in
id └─┘ └┘ └──┘
src └┘
typ └─┘ └┘ └──┘
347 lcm_eq_normalize
id └──────────────┘
src └──────────────┘
typ └──────────────┘
348 (lcm_dvd (mul_dvd_mul_left a (dvd_lcm_left _ _)) (mul_dvd_mul_left a (dvd_lcm_right _ _)))
id └─────┘ └──────────────┘ ┴ └──────────┘ └──────────────┘ ┴ └───────────┘
src └─────┘ └──────────────┘ └──────────┘ └──────────────┘ └───────────┘
typ └─────┘ └──────────────┘ ┴ └──────────┘ └──────────────┘ ┴ └───────────┘
349 (eq.symm ▸ (mul_dvd_mul_left a $ lcm_dvd
id └───┘ ┴ └──────────────┘ ┴ └─────┘
src └───┘ ┴ └──────────────┘ └─────┘
typ └───┘ ┴ └──────────────┘ ┴ └─────┘
350 ((mul_dvd_mul_iff_left ha).1 $ eq ▸ dvd_lcm_left _ _)
id └──────────────────┘ └┘ ┴ ┴ └──────────┘
src └──────────────────┘ ┴ ┴ └──────────┘
typ └──────────────────┘ └┘ ┴ ┴ └──────────┘
doc └──────────────────┘
351 ((mul_dvd_mul_iff_left ha).1 $ eq ▸ dvd_lcm_right _ _)))
id └──────────────────┘ └┘ ┴ ┴ └───────────┘
src └──────────────────┘ ┴ ┴ └───────────┘
typ └──────────────────┘ └┘ ┴ ┴ └───────────┘
doc └──────────────────┘
352
353 @[simp] theorem lcm_mul_right (a b c : α) : lcm (b * a) (c * a) = lcm b c * normalize a :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───────┘ ┴
src └─┘ ┴ ┴ ┴ └─┘ ┴ └───────┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └───────┘ ┴
doc └──┘
354 by simp only [mul_comm, lcm_mul_left]
id └──────┘ └──────────┘
src └─────────┘└──────┘└┘└──────────┘└─
typ └─────────┘└──────┘└┘└──────────┘└─
doc └─────────┘ └┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └───────────────────────────────────
355
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
356 theorem lcm_eq_left_iff (a b : α) (h : normalize a = a) : lcm a b = a ↔ b ∣ a :=
id ┴ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ └─┘ ┴ ┴ ┴
typ ┴ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
357 iff.intro (assume eq, eq ▸ dvd_lcm_right _ _) $
id └───────┘ └┘ └┘ ┴ └───────────┘
src └───────┘ └┘ └┘ ┴ └───────────┘
typ └───────┘ └┘ └┘ ┴ └───────────┘
358 assume hab, dvd_antisymm_of_normalize_eq (normalize_lcm _ _) h (lcm_dvd (dvd_refl a) hab) (dvd_lcm_left _ _)
id └─┘ └──────────────────────────┘ └───────────┘ ┴ └─────┘ └──────┘ ┴ └─┘ └──────────┘
src └──────────────────────────┘ └───────────┘ └─────┘ └──────┘ └──────────┘
typ └─┘ └──────────────────────────┘ └───────────┘ ┴ └─────┘ └──────┘ ┴ └─┘ └──────────┘
359
360 theorem lcm_eq_right_iff (a b : α) (h : normalize b = b) : lcm a b = b ↔ a ∣ b :=
id ┴ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src └───────┘ ┴ └─┘ ┴ ┴ ┴
typ ┴ └───────┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
361 by simpa only [lcm_comm b a] using lcm_eq_left_iff b a h
id └──────┘ ┴ ┴ └─────────────┘ ┴ ┴ ┴
src └──────────┘└──────┘┴ ┴ └──────┘└─────────────┘┴ ┴ ┴ └
typ └──────────┘└──────┘┴┴┴┴└──────┘└─────────────┘┴┴┴┴┴┴└
doc └──────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ └
txt └──────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ └
par └──────────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ └
pid ┴└──┘└┘ ┴ ┴ ┴┴└────┘ ┴ ┴ ┴ └
st └──────────────────────────────────────────────────────
362
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
363 theorem lcm_dvd_lcm_mul_left (m n k : α) : lcm m n ∣ lcm (k * m) n :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
364 lcm_dvd_lcm (dvd_mul_left _ _) (dvd_refl _)
id └─────────┘ └──────────┘ └──────┘
src └─────────┘ └──────────┘ └──────┘
typ └─────────┘ └──────────┘ └──────┘
365
366 theorem lcm_dvd_lcm_mul_right (m n k : α) : lcm m n ∣ lcm (m * k) n :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
367 lcm_dvd_lcm (dvd_mul_right _ _) (dvd_refl _)
id └─────────┘ └───────────┘ └──────┘
src └─────────┘ └───────────┘ └──────┘
typ └─────────┘ └───────────┘ └──────┘
368
369 theorem lcm_dvd_lcm_mul_left_right (m n k : α) : lcm m n ∣ lcm m (k * n) :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
370 lcm_dvd_lcm (dvd_refl _) (dvd_mul_left _ _)
id └─────────┘ └──────┘ └──────────┘
src └─────────┘ └──────┘ └──────────┘
typ └─────────┘ └──────┘ └──────────┘
371
372 theorem lcm_dvd_lcm_mul_right_right (m n k : α) : lcm m n ∣ lcm m (n * k) :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src └─┘ ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
373 lcm_dvd_lcm (dvd_refl _) (dvd_mul_right _ _)
id └─────────┘ └──────┘ └───────────┘
src └─────────┘ └──────┘ └───────────┘
typ └─────────┘ └──────┘ └───────────┘
374
375 end lcm
376
377 end gcd_domain
378
379 namespace int
380
381 section normalization_domain
382
383 instance : normalization_domain ℤ :=
id └──────────────────┘ ┴
src └──────────────────┘ ┴
typ └──────────────────┘ ┴
doc └──────────────────┘
384 { norm_unit := λa:ℤ, if 0 ≤ a then 1 else -1,
id ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴
385 norm_unit_zero := if_pos (le_refl _),
id └────┘ └─────┘
src └────┘ └─────┘
typ └────┘ └─────┘
386 norm_unit_mul := assume a b hna hnb,
id ┴ ┴ └─┘ └─┘
typ ┴ ┴ └─┘ └─┘
387 begin
st └─────
388 by_cases ha : 0 ≤ a; by_cases hb : 0 ≤ b; simp [ha, hb],
id ┴ ┴ ┴ └┘ └┘
src └───────┘ └───┘┴┴ └───────┘ └───┘ ┴ └────┘ └┘ ┴
typ └───────┘ └───┘┴┴┴ └───────┘ └───┘ ┴┴ └────┘└┘└┘└┘┴
doc └───────┘ └───┘ ┴ └───────┘ └───┘ ┴ └────┘ └┘ ┴
txt └───────┘ └───┘ ┴ └───────┘ └───┘ ┴ └────┘ └┘ ┴
par └───────┘ └───┘ ┴ └───────┘ └───┘ ┴ └────┘ └┘ ┴
pid ┴ └───┘ ┴ ┴ └───┘ ┴ ┴┴ └┘ ┴
st ──────────────────────────────────────────────────────────┘└─
389 exact if_pos (mul_nonneg ha hb),
id └────┘ └────────┘ └┘ └┘
src └────┘└────┘┴ └────────┘┴ ┴ ┴
typ └────┘└────┘┴ └────────┘┴└┘┴└┘┴
doc └────┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────┘└─
390 exact if_neg (assume h, hb $ nonneg_of_mul_nonneg_left h $ lt_of_le_of_ne ha hna.symm),
id └────┘ └┘ └───────────────────────┘ └────────────┘ └┘ └──────┘
src └────┘└────┘┴ └──┘ ┴ ┴└───────────────────────┘┴ ┴ ┴└────────────┘┴ ┴└──────┘┴
typ └────┘└────┘┴ └──┘└┘┴ ┴└───────────────────────┘┴ ┴ ┴└────────────┘┴└┘┴└──────┘┴
doc └────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────────────────────────────────────────────────────────┘└─
391 exact if_neg (assume h, ha $ nonneg_of_mul_nonneg_right h $ lt_of_le_of_ne hb hnb.symm),
id └────┘ └┘ └────────────────────────┘ └────────────┘ └┘ └──────┘
src └────┘└────┘┴ └──┘ ┴ ┴└────────────────────────┘┴ ┴ ┴└────────────┘┴ ┴└──────┘┴
typ └────┘└────┘┴ └──┘└┘┴ ┴└────────────────────────┘┴ ┴ ┴└────────────┘┴└┘┴└──────┘┴
doc └────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
txt └────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
par └────┘ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ └──┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ──────────────────────────────────────────────────────────────────────────────────────────┘└─
392 exact if_pos (mul_nonneg_of_nonpos_of_nonpos (le_of_not_ge ha) (le_of_not_ge hb))
id └────┘ └────────────────────────────┘ └┘ └──────────┘ └┘
src └────┘└────┘┴ └────────────────────────────┘┴ ┴ └┘ └──────────┘┴ └──
typ └────┘└────┘┴ └────────────────────────────┘┴ ┴└┘└┘ └──────────┘┴└┘└──
doc └────┘ ┴ ┴ ┴ └┘ ┴ └──
txt └────┘ ┴ ┴ ┴ └┘ ┴ └──
par └────┘ ┴ ┴ ┴ └┘ ┴ └──
pid ┴ ┴ ┴ ┴ └┘ ┴ └┘└
st ──────────────────────────────────────────────────────────────────────────────────────
393 end,
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘└─┘
394 norm_unit_coe_units := assume u, (units_eq_one_or u).elim
id ┴ └─────────────┘ ┴ └──┘
src └─────────────┘ └──┘
typ ┴ └─────────────┘ ┴ └──┘
395 (assume eq, eq.symm ▸ if_pos zero_le_one)
id └┘ └┘└───┘ ┴ └────┘ └─────────┘
src └┘ └┘└───┘ ┴ └────┘ └─────────┘
typ └┘ └┘└───┘ ┴ └────┘ └─────────┘
396 (assume eq, eq.symm ▸ if_neg (not_le_of_gt $ show (-1:ℤ) < 0, by simp [@neg_lt ℤ _ 1 0])),
id └┘ └┘└───┘ ┴ └────┘ └──────────┘ ┴ ┴ ┴ └────┘
src └┘ └┘└───┘ ┴ └────┘ └──────────┘ ┴ ┴ ┴ └────┘ └────┘┴ └─────┘
typ └┘ └┘└───┘ ┴ └────┘ └──────────┘ ┴ ┴ ┴ └────┘ └────┘┴ └─────┘
doc └────┘ ┴ └─────┘
txt └────┘ ┴ └─────┘
par └────┘ ┴ └─────┘
pid ┴┴ ┴ └─────┘
st └─────────────────────┘
397 .. (infer_instance : integral_domain ℤ) }
id └────────────┘ └─────────────┘ ┴
src └────────────┘ └─────────────┘ ┴
typ └────────────┘ └─────────────┘ ┴
doc └────────────┘
398
399 lemma normalize_of_nonneg {z : ℤ} (h : 0 ≤ z) : normalize z = z :=
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
src ┴ ┴ └───────┘ ┴
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴
400 show z * ↑(ite _ _ _) = z, by rw [if_pos h, units.coe_one, mul_one]
id ┴ ┴ ┴ └─┘ ┴ ┴ └────┘ ┴ └───────────┘ └─────┘
src ┴ ┴ └─┘ ┴ └──┘└────┘┴ └┘└───────────┘└┘└─────┘└─
typ ┴ ┴ ┴ └─┘ ┴ ┴ └──┘└────┘┴┴└┘└───────────┘└┘└─────┘└─
doc └──┘ ┴ └┘ └┘ └─
txt └──┘ ┴ └┘ └┘ └─
par └──┘ ┴ └┘ └┘ └─
pid └┘ ┴ └┘ └┘ ┴└
st └───────────┘└─────────────┘└───────┘┴└
401
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
402 lemma normalize_of_neg {z : ℤ} (h : z < 0) : normalize z = -z :=
id ┴ ┴ ┴ └───────┘ ┴ ┴ ┴┴
src ┴ ┴ └───────┘ ┴ ┴
typ ┴ ┴ ┴ └───────┘ ┴ ┴ ┴┴
403 show z * ↑(ite _ _ _) = -z, by rw [if_neg (not_le_of_gt h), units.coe_neg, units.coe_one, mul_neg_one]
id ┴ ┴ ┴ └─┘ ┴ ┴┴ └────┘ └──────────┘ ┴ └───────────┘ └───────────┘ └─────────┘
src ┴ ┴ └─┘ ┴ ┴ └──┘└────┘┴ └──────────┘┴ └─┘└───────────┘└┘└───────────┘└┘└─────────┘└─
typ ┴ ┴ ┴ └─┘ ┴ ┴┴ └──┘└────┘┴ └──────────┘┴┴└─┘└───────────┘└┘└───────────┘└┘└─────────┘└─
doc └──┘ ┴ ┴ └─┘└───────────┘└┘ └┘└─────────┘└─
txt └──┘ ┴ ┴ └─┘ └┘ └┘ └─
par └──┘ ┴ ┴ └─┘ └┘ └┘ └─
pid └┘ ┴ ┴ └─┘ └┘ └┘ ┴└
st └──────────────────────────┘└─────────────┘└─────────────┘└───────────┘┴└
404
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
405 lemma normalize_coe_nat (n : ℕ) : normalize (n : ℤ) = n :=
id ┴ └───────┘ ┴ ┴ ┴ ┴
src ┴ └───────┘ ┴ ┴
typ ┴ └───────┘ ┴ ┴ ┴ ┴
406 normalize_of_nonneg (coe_nat_le_coe_nat_of_le $ nat.zero_le n)
id └─────────────────┘ └──────────────────────┘ └─────────┘ ┴
src └─────────────────┘ └──────────────────────┘ └─────────┘
typ └─────────────────┘ └──────────────────────┘ └─────────┘ ┴
407
408 theorem coe_nat_abs_eq_normalize (z : ℤ) : (z.nat_abs : ℤ) = normalize z :=
id ┴ ┴└──────┘ ┴ ┴ └───────┘ ┴
src ┴ └──────┘ ┴ ┴ └───────┘
typ ┴ ┴└──────┘ ┴ ┴ └───────┘ ┴
409 begin
st └─────
410 by_cases 0 ≤ z,
id ┴ ┴
src └─────────┘┴┴
typ └─────────┘┴┴┴
doc └─────────┘ ┴
txt └─────────┘ ┴
par └─────────┘ ┴
pid └─┘ ┴
st ───────────────┘└─
411 { simp [nat_abs_of_nonneg h, normalize_of_nonneg h] },
id └───────────────┘ ┴ └─────────────────┘ ┴
src └────┘└───────────────┘┴ └┘└─────────────────┘┴ └┘
typ └────┘└───────────────┘┴┴└┘└─────────────────┘┴┴└┘
doc └────┘ ┴ └┘ ┴ └┘
txt └────┘ ┴ └┘ ┴ └┘
par └────┘ ┴ └┘ ┴ └┘
pid ┴┴ ┴ └┘ ┴ ┴┴
st ───┘└────────────────────────────────────────────────┘└┘└
412 { simp [of_nat_nat_abs_of_nonpos (le_of_not_ge h), normalize_of_neg (lt_of_not_ge h)] }
id └──────────────────────┘ └──────────┘ ┴ └──────────────┘ └──────────┘ ┴
src └────┘└──────────────────────┘┴ └──────────┘┴ └─┘└──────────────┘┴ └──────────┘┴ └─┘
typ └────┘└──────────────────────┘┴ └──────────┘┴┴└─┘└──────────────┘┴ └──────────┘┴┴└─┘
doc └────┘ ┴ ┴ └─┘ ┴ ┴ └─┘
txt └────┘ ┴ ┴ └─┘ ┴ ┴ └─┘
par └────┘ ┴ ┴ └─┘ ┴ ┴ └─┘
pid ┴┴ ┴ ┴ └─┘ ┴ ┴ └┘┴
st ───────────────────────────────────────────────────────────────────────────────────────┘└─
413 end
st ──┘
414
415 end normalization_domain
416
417 /-- ℤ specific version of least common multiple. -/
418 def lcm (i j : ℤ) : ℕ := nat.lcm (nat_abs i) (nat_abs j)
id ┴ ┴ └─────┘ └─────┘ ┴ └─────┘ ┴
src ┴ ┴ └─────┘ └─────┘ └─────┘
typ ┴ ┴ └─────┘ └─────┘ ┴ └─────┘ ┴
419
420 theorem lcm_def (i j : ℤ) : lcm i j = nat.lcm (nat_abs i) (nat_abs j) := rfl
id ┴ └─┘ ┴ ┴ ┴ └─────┘ └─────┘ ┴ └─────┘ ┴ └─┘
src ┴ └─┘ ┴ └─────┘ └─────┘ └─────┘ └─┘
typ ┴ └─┘ ┴ ┴ ┴ └─────┘ └─────┘ ┴ └─────┘ ┴ └─┘
doc └─┘
421
422 section gcd_domain
423
424 theorem gcd_dvd_left (i j : ℤ) : (gcd i j : ℤ) ∣ i :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
425 dvd_nat_abs.mp $ coe_nat_dvd.mpr $ nat.gcd_dvd_left _ _
id └─────────┘└─┘ └─────────┘└──┘ └──────────────┘
src └─────────┘└─┘ └─────────┘└──┘ └──────────────┘
typ └─────────┘└─┘ └─────────┘└──┘ └──────────────┘
426
427 theorem gcd_dvd_right (i j : ℤ) : (gcd i j : ℤ) ∣ j :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
428 dvd_nat_abs.mp $ coe_nat_dvd.mpr $ nat.gcd_dvd_right _ _
id └─────────┘└─┘ └─────────┘└──┘ └───────────────┘
src └─────────┘└─┘ └─────────┘└──┘ └───────────────┘
typ └─────────┘└─┘ └─────────┘└──┘ └───────────────┘
429
430 theorem dvd_gcd {i j k : ℤ} (h1 : k ∣ i) (h2 : k ∣ j) : k ∣ gcd i j :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
431 nat_abs_dvd.1 $ coe_nat_dvd.2 $ nat.dvd_gcd (nat_abs_dvd_abs_iff.2 h1) (nat_abs_dvd_abs_iff.2 h2)
id └─────────┘┴ └─────────┘┴ └─────────┘ └─────────────────┘┴ └┘ └─────────────────┘┴ └┘
src └─────────┘┴ └─────────┘┴ └─────────┘ └─────────────────┘┴ └─────────────────┘┴
typ └─────────┘┴ └─────────┘┴ └─────────┘ └─────────────────┘┴ └┘ └─────────────────┘┴ └┘
432
433 theorem gcd_mul_lcm (i j : ℤ) : gcd i j * lcm i j = nat_abs (i * j) :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴
src ┴ └─┘ ┴ └─┘ ┴ └─────┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴ ┴ ┴
doc └─┘
434 by rw [int.gcd, int.lcm, nat.gcd_mul_lcm, nat_abs_mul]
id └─────┘ └─────┘ └─────────────┘ └─────────┘
src └──┘└─────┘└┘└─────┘└┘└─────────────┘└┘└─────────┘└─
typ └──┘└─────┘└┘└─────┘└┘└─────────────┘└┘└─────────┘└─
doc └──┘ └┘└─────┘└┘ └┘ └─
txt └──┘ └┘ └┘ └┘ └─
par └──┘ └┘ └┘ └┘ └─
pid └┘ └┘ └┘ └┘ ┴└
st └──────────┘└───────┘└───────────────┘└───────────┘┴└
435
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
436 instance : gcd_domain ℤ :=
id └────────┘ ┴
src └────────┘ ┴
typ └────────┘ ┴
doc └────────┘
437 { gcd := λa b, int.gcd a b,
id ┴ ┴ └─────┘ ┴ ┴
src └─────┘
typ ┴ ┴ └─────┘ ┴ ┴
438 lcm := λa b, int.lcm a b,
id ┴ ┴ └─────┘ ┴ ┴
src └─────┘
typ ┴ ┴ └─────┘ ┴ ┴
doc └─────┘
439 gcd_dvd_left := assume a b, int.gcd_dvd_left _ _,
id ┴ ┴ └──────────────┘
src └──────────────┘
typ ┴ ┴ └──────────────┘
440 gcd_dvd_right := assume a b, int.gcd_dvd_right _ _,
id ┴ ┴ └───────────────┘
src └───────────────┘
typ ┴ ┴ └───────────────┘
441 dvd_gcd := assume a b c, dvd_gcd,
id ┴ ┴ ┴ └─────┘
src └─────┘
typ ┴ ┴ ┴ └─────┘
442 normalize_gcd := assume a b, normalize_coe_nat _,
id ┴ ┴ └───────────────┘
src └───────────────┘
typ ┴ ┴ └───────────────┘
443 gcd_mul_lcm := by intros; rw [← int.coe_nat_mul, gcd_mul_lcm, coe_nat_abs_eq_normalize],
id └─────────────┘ └─────────┘ └──────────────────────┘
src └────┘ └────┘└─────────────┘└┘└─────────┘└┘└──────────────────────┘┴
typ └────┘ └────┘└─────────────┘└┘└─────────┘└┘└──────────────────────┘┴
doc └────┘ └────┘ └┘ └┘ ┴
txt └────┘ └────┘ └┘ └┘ ┴
par └────┘ └────┘ └┘ └┘ ┴
pid └──┘ └┘ └┘ ┴
st └───────────┘└───────────────┘└───────────┘└────────────────────────┘┴
444 lcm_zero_left := assume a, coe_nat_eq_zero.2 $ nat.lcm_zero_left _,
id ┴ └─────────────┘┴ └───────────────┘
src └─────────────┘┴ └───────────────┘
typ ┴ └─────────────┘┴ └───────────────┘
445 lcm_zero_right := assume a, coe_nat_eq_zero.2 $ nat.lcm_zero_right _,
id ┴ └─────────────┘┴ └────────────────┘
src └─────────────┘┴ └────────────────┘
typ ┴ └─────────────┘┴ └────────────────┘
446 .. int.normalization_domain }
id └──────────────────────┘
src └──────────────────────┘
typ └──────────────────────┘
447
448 lemma coe_gcd (i j : ℤ) : ↑(int.gcd i j) = gcd_domain.gcd i j := rfl
id ┴ ┴ └─────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ └─┘
src ┴ ┴ └─────┘ ┴ └────────────┘ └─┘
typ ┴ ┴ └─────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ └─┘
449 lemma coe_lcm (i j : ℤ) : ↑(int.lcm i j) = gcd_domain.lcm i j := rfl
id ┴ ┴ └─────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ └─┘
src ┴ ┴ └─────┘ ┴ └────────────┘ └─┘
typ ┴ ┴ └─────┘ ┴ ┴ ┴ └────────────┘ ┴ ┴ └─┘
doc └─────┘
450
451 lemma nat_abs_gcd (i j : ℤ) : nat_abs (gcd_domain.gcd i j) = int.gcd i j := rfl
id ┴ └─────┘ └────────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘
src ┴ └─────┘ └────────────┘ ┴ └─────┘ └─┘
typ ┴ └─────┘ └────────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘
452 lemma nat_abs_lcm (i j : ℤ) : nat_abs (gcd_domain.lcm i j) = int.lcm i j := rfl
id ┴ └─────┘ └────────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘
src ┴ └─────┘ └────────────┘ ┴ └─────┘ └─┘
typ ┴ └─────┘ └────────────┘ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘
doc └─────┘
453
454 end gcd_domain
455
456 theorem gcd_comm (i j : ℤ) : gcd i j = gcd j i := nat.gcd_comm _ _
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──────────┘
src ┴ └─┘ ┴ └─┘ └──────────┘
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ └──────────┘
457
458 theorem gcd_assoc (i j k : ℤ) : gcd (gcd i j) k = gcd i (gcd j k) := nat.gcd_assoc _ _ _
id ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ └───────────┘
src ┴ └─┘ └─┘ ┴ └─┘ └─┘ └───────────┘
typ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴ └───────────┘
459
460 @[simp] theorem gcd_self (i : ℤ) : gcd i i = nat_abs i := by simp [gcd]
id ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴ └─┘
src ┴ └─┘ ┴ └─────┘ └────┘└─┘└─
typ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴ └────┘└─┘└─
doc └──┘ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
461
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
462 @[simp] theorem gcd_zero_left (i : ℤ) : gcd 0 i = nat_abs i := by simp [gcd]
id ┴ └─┘ ┴ ┴ └─────┘ ┴ └─┘
src ┴ └─┘ ┴ └─────┘ └────┘└─┘└─
typ ┴ └─┘ ┴ ┴ └─────┘ ┴ └────┘└─┘└─
doc └──┘ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
463
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
464 @[simp] theorem gcd_zero_right (i : ℤ) : gcd i 0 = nat_abs i := by simp [gcd]
id ┴ └─┘ ┴ ┴ └─────┘ ┴ └─┘
src ┴ └─┘ ┴ └─────┘ └────┘└─┘└─
typ ┴ └─┘ ┴ ┴ └─────┘ ┴ └────┘└─┘└─
doc └──┘ └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └───────────
465
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
466 @[simp] theorem gcd_one_left (i : ℤ) : gcd 1 i = 1 := nat.gcd_one_left _
id ┴ └─┘ ┴ ┴ └──────────────┘
src ┴ └─┘ ┴ └──────────────┘
typ ┴ └─┘ ┴ ┴ └──────────────┘
doc └──┘
467
468 @[simp] theorem gcd_one_right (i : ℤ) : gcd i 1 = 1 := nat.gcd_one_right _
id ┴ └─┘ ┴ ┴ └───────────────┘
src ┴ └─┘ ┴ └───────────────┘
typ ┴ └─┘ ┴ ┴ └───────────────┘
doc └──┘
469
470 theorem gcd_mul_left (i j k : ℤ) : gcd (i * j) (i * k) = nat_abs i * gcd j k :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─────┘ ┴ ┴ └─┘ ┴ ┴
471 by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_gcd, coe_nat_abs_eq_normalize]
id └────────────────────────┘ └─────┘ └──────────────────────┘
src └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
typ └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
doc └────┘ └──────────┘ └┘ └─
txt └────┘ └──────────┘ └┘ └─
par └────┘ └──────────┘ └┘ └─
pid ┴┴ └──────────┘ └┘ ┴└
st └────────────────────────────────────────────────────────────────────────────────
472
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
473 theorem gcd_mul_right (i j k : ℤ) : gcd (i * j) (k * j) = gcd i k * nat_abs j :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴
src ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ └─────┘
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴
474 by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_gcd, coe_nat_abs_eq_normalize]
id └────────────────────────┘ └─────┘ └──────────────────────┘
src └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
typ └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
doc └────┘ └──────────┘ └┘ └─
txt └────┘ └──────────┘ └┘ └─
par └────┘ └──────────┘ └┘ └─
pid ┴┴ └──────────┘ └┘ ┴└
st └────────────────────────────────────────────────────────────────────────────────
475
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
476 theorem gcd_pos_of_non_zero_left {i : ℤ} (j : ℤ) (i_non_zero : i ≠ 0) : 0 < gcd i j :=
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
477 nat.gcd_pos_of_pos_left (nat_abs j) (nat_abs_pos_of_ne_zero i_non_zero)
id └─────────────────────┘ └─────┘ ┴ └────────────────────┘ └────────┘
src └─────────────────────┘ └─────┘ └────────────────────┘
typ └─────────────────────┘ └─────┘ ┴ └────────────────────┘ └────────┘
478
479 theorem gcd_pos_of_non_zero_right (i : ℤ) {j : ℤ} (j_non_zero : j ≠ 0) : 0 < gcd i j :=
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴
480 nat.gcd_pos_of_pos_right (nat_abs i) (nat_abs_pos_of_ne_zero j_non_zero)
id └──────────────────────┘ └─────┘ ┴ └────────────────────┘ └────────┘
src └──────────────────────┘ └─────┘ └────────────────────┘
typ └──────────────────────┘ └─────┘ ┴ └────────────────────┘ └────────┘
481
482 theorem gcd_eq_zero_iff {i j : ℤ} : gcd i j = 0 ↔ i = 0 ∧ j = 0 :=
id ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ ┴ ┴ ┴ ┴
typ ┴ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴ ┴
483 by rw [← int.coe_nat_eq_coe_nat_iff, int.coe_nat_zero, coe_gcd, gcd_eq_zero_iff]
id └────────────────────────┘ └──────────────┘ └─────┘ └─────────────┘
src └────┘└────────────────────────┘└┘└──────────────┘└┘└─────┘└┘└─────────────┘└─
typ └────┘└────────────────────────┘└┘└──────────────┘└┘└─────┘└┘└─────────────┘└─
doc └────┘ └┘ └┘ └┘ └─
txt └────┘ └┘ └┘ └┘ └─
par └────┘ └┘ └┘ └┘ └─
pid └──┘ └┘ └┘ └┘ ┴└
st └───────────────────────────────┘└────────────────┘└───────┘└───────────────┘┴└
484
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
485 theorem gcd_div {i j k : ℤ} (H1 : k ∣ i) (H2 : k ∣ j) :
id ┴ ┴ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴
486 gcd (i / k) (j / k) = gcd i j / nat_abs k :=
id └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴
src └─┘ ┴ ┴ ┴ └─┘ ┴ └─────┘
typ └─┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴
487 by rw [gcd, nat_abs_div i k H1, nat_abs_div j k H2];
id └─┘ └─────────┘ ┴ ┴ └┘ └─────────┘ ┴ ┴ └┘
src └──┘└─┘└┘└─────────┘┴ ┴ ┴ └┘└─────────┘┴ ┴ ┴ ┴
typ └──┘└─┘└┘└─────────┘┴┴┴┴┴└┘└┘└─────────┘┴┴┴┴┴└┘┴
doc └──┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
txt └──┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
par └──┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
pid └┘ └┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴
st └──────┘└──────────────────┘└──────────────────┘┴└─
488 exact nat.gcd_div (nat_abs_dvd_abs_iff.mpr H1) (nat_abs_dvd_abs_iff.mpr H2)
id └─────────┘ └┘ └─────────────────────┘ └┘
src └────┘└─────────┘┴ ┴ └┘ └─────────────────────┘┴ └─
typ └────┘└─────────┘┴ ┴└┘└┘ └─────────────────────┘┴└┘└─
doc └────┘ ┴ ┴ └┘ ┴ └─
txt └────┘ ┴ ┴ └┘ ┴ └─
par └────┘ ┴ ┴ └┘ ┴ └─
pid ┴ ┴ ┴ └┘ ┴ ┴└
st ────────────────────────────────────────────────────────────────────────────
489
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
490 theorem gcd_dvd_gcd_of_dvd_left {i k : ℤ} (j : ℤ) (H : i ∣ k) : gcd i j ∣ gcd k j :=
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴ └─┘ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
491 int.coe_nat_dvd.1 $ dvd_gcd (dvd.trans (gcd_dvd_left i j) H) (gcd_dvd_right i j)
id └─────────────┘┴ └─────┘ └───────┘ └──────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴
src └─────────────┘┴ └─────┘ └───────┘ └──────────┘ └───────────┘
typ └─────────────┘┴ └─────┘ └───────┘ └──────────┘ ┴ ┴ ┴ └───────────┘ ┴ ┴
492
493 theorem gcd_dvd_gcd_of_dvd_right {i k : ℤ} (j : ℤ) (H : i ∣ k) : gcd j i ∣ gcd j k :=
id ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ ┴ ┴ └─┘ ┴ └─┘
typ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
494 int.coe_nat_dvd.1 $ dvd_gcd (gcd_dvd_left j i) (dvd.trans (gcd_dvd_right j i) H)
id └─────────────┘┴ └─────┘ └──────────┘ ┴ ┴ └───────┘ └───────────┘ ┴ ┴ ┴
src └─────────────┘┴ └─────┘ └──────────┘ └───────┘ └───────────┘
typ └─────────────┘┴ └─────┘ └──────────┘ ┴ ┴ └───────┘ └───────────┘ ┴ ┴ ┴
495
496 theorem gcd_dvd_gcd_mul_left (i j k : ℤ) : gcd i j ∣ gcd (k * i) j :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
497 gcd_dvd_gcd_of_dvd_left _ (dvd_mul_left _ _)
id └─────────────────────┘ └──────────┘
src └─────────────────────┘ └──────────┘
typ └─────────────────────┘ └──────────┘
498
499 theorem gcd_dvd_gcd_mul_right (i j k : ℤ) : gcd i j ∣ gcd (i * k) j :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
500 gcd_dvd_gcd_of_dvd_left _ (dvd_mul_right _ _)
id └─────────────────────┘ └───────────┘
src └─────────────────────┘ └───────────┘
typ └─────────────────────┘ └───────────┘
501
502 theorem gcd_dvd_gcd_mul_left_right (i j k : ℤ) : gcd i j ∣ gcd i (k * j) :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
503 gcd_dvd_gcd_of_dvd_right _ (dvd_mul_left _ _)
id └──────────────────────┘ └──────────┘
src └──────────────────────┘ └──────────┘
typ └──────────────────────┘ └──────────┘
504
505 theorem gcd_dvd_gcd_mul_right_right (i j k : ℤ) : gcd i j ∣ gcd i (j * k) :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
src ┴ └─┘ ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
506 gcd_dvd_gcd_of_dvd_right _ (dvd_mul_right _ _)
id └──────────────────────┘ └───────────┘
src └──────────────────────┘ └───────────┘
typ └──────────────────────┘ └───────────┘
507
508 theorem gcd_eq_left {i j : ℤ} (H : i ∣ j) : gcd i j = nat_abs i :=
id ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴
src ┴ ┴ └─┘ ┴ └─────┘
typ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴
509 nat.dvd_antisymm (by unfold gcd; exact nat.gcd_dvd_left _ _)
id └──────────────┘ └──────────────┘
src └──────────────┘ └────────┘ └────┘└──────────────┘└──┘
typ └──────────────┘ └────────┘ └────┘└──────────────┘└──┘
doc └────────┘ └────┘ └──┘
txt └────────┘ └────┘ └──┘
par └────────┘ └────┘ └──┘
pid └──┘ ┴ └──┘
st └─────────────────────────────────────┘
510 (by unfold gcd; exact nat.dvd_gcd (dvd_refl _) (nat_abs_dvd_abs_iff.mpr H))
id └─────────┘ └──────┘ └─────────────────────┘ ┴
src └────────┘ └────┘└─────────┘┴ └──────┘└──┘ └─────────────────────┘┴ ┴
typ └────────┘ └────┘└─────────┘┴ └──────┘└──┘ └─────────────────────┘┴┴┴
doc └────────┘ └────┘ ┴ └──┘ ┴ ┴
txt └────────┘ └────┘ ┴ └──┘ ┴ ┴
par └────────┘ └────┘ ┴ └──┘ ┴ ┴
pid └──┘ ┴ ┴ └──┘ ┴ ┴
st └─────────────────────────────────────────────────────────────────────┘
511
512 theorem gcd_eq_right {i j : ℤ} (H : j ∣ i) : gcd i j = nat_abs j :=
id ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴
src ┴ ┴ └─┘ ┴ └─────┘
typ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴
513 by rw [gcd_comm, gcd_eq_left H]
id └──────┘ └─────────┘ ┴
src └──┘└──────┘└┘└─────────┘┴ └─
typ └──┘└──────┘└┘└─────────┘┴┴└─
doc └──┘ └┘ ┴ └─
txt └──┘ └┘ ┴ └─
par └──┘ └┘ ┴ └─
pid └┘ └┘ ┴ ┴└
st └───────────┘└─────────────┘┴└
514
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
515 /- lcm -/
src ──────────
typ ──────────
doc ──────────
txt ──────────
par ──────────
pid ──────────
st ──────────
516
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
517 theorem lcm_comm (i j : ℤ) : lcm i j = lcm j i :=
id ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ └─┘ ┴ └─┘
typ ┴ └─┘ ┴ ┴ ┴ └─┘ ┴ ┴
doc └─┘ └─┘
518 by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_lcm, lcm_comm]
id └────────────────────────┘ └─────┘ └──────┘
src └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────┘└─
typ └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────┘└─
doc └────┘ └──────────┘ └┘ └─
txt └────┘ └──────────┘ └┘ └─
par └────┘ └──────────┘ └┘ └─
pid ┴┴ └──────────┘ └┘ ┴└
st └────────────────────────────────────────────────────────────────
519
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
520 theorem lcm_assoc (i j k : ℤ) : lcm (lcm i j) k = lcm i (lcm j k) :=
id ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
src ┴ └─┘ └─┘ ┴ └─┘ └─┘
typ ┴ └─┘ └─┘ ┴ ┴ ┴ ┴ └─┘ ┴ └─┘ ┴ ┴
doc └─┘ └─┘ └─┘ └─┘
521 by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_lcm, lcm_assoc]
id └────────────────────────┘ └─────┘ └───────┘
src └────┘ └────────────────────────┘└──────────┘└─────┘└┘└───────┘└─
typ └────┘ └────────────────────────┘└──────────┘└─────┘└┘└───────┘└─
doc └────┘ └──────────┘ └┘ └─
txt └────┘ └──────────┘ └┘ └─
par └────┘ └──────────┘ └┘ └─
pid ┴┴ └──────────┘ └┘ ┴└
st └─────────────────────────────────────────────────────────────────
522
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
523 @[simp] theorem lcm_zero_left (i : ℤ) : lcm 0 i = 0 :=
id ┴ └─┘ ┴ ┴
src ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴
doc └──┘ └─┘
524 by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_lcm]
id └────────────────────────┘ └─────┘
src └────┘ └────────────────────────┘└──────────┘└─────┘└─
typ └────┘ └────────────────────────┘└──────────┘└─────┘└─
doc └────┘ └──────────┘ └─
txt └────┘ └──────────┘ └─
par └────┘ └──────────┘ └─
pid ┴┴ └──────────┘ ┴└
st └──────────────────────────────────────────────────────
525
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
526 @[simp] theorem lcm_zero_right (i : ℤ) : lcm i 0 = 0 :=
id ┴ └─┘ ┴ ┴
src ┴ └─┘ ┴
typ ┴ └─┘ ┴ ┴
doc └──┘ └─┘
527 by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_lcm]
id └────────────────────────┘ └─────┘
src └────┘ └────────────────────────┘└──────────┘└─────┘└─
typ └────┘ └────────────────────────┘└──────────┘└─────┘└─
doc └────┘ └──────────┘ └─
txt └────┘ └──────────┘ └─
par └────┘ └──────────┘ └─
pid ┴┴ └──────────┘ ┴└
st └──────────────────────────────────────────────────────
528
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
529 @[simp] theorem lcm_one_left (i : ℤ) : lcm 1 i = nat_abs i :=
id ┴ └─┘ ┴ ┴ └─────┘ ┴
src ┴ └─┘ ┴ └─────┘
typ ┴ └─┘ ┴ ┴ └─────┘ ┴
doc └──┘ └─┘
530 by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_lcm, coe_nat_abs_eq_normalize]
id └────────────────────────┘ └─────┘ └──────────────────────┘
src └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
typ └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
doc └────┘ └──────────┘ └┘ └─
txt └────┘ └──────────┘ └┘ └─
par └────┘ └──────────┘ └┘ └─
pid ┴┴ └──────────┘ └┘ ┴└
st └────────────────────────────────────────────────────────────────────────────────
531
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
532 @[simp] theorem lcm_one_right (i : ℤ) : lcm i 1 = nat_abs i :=
id ┴ └─┘ ┴ ┴ └─────┘ ┴
src ┴ └─┘ ┴ └─────┘
typ ┴ └─┘ ┴ ┴ └─────┘ ┴
doc └──┘ └─┘
533 by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_lcm, coe_nat_abs_eq_normalize]
id └────────────────────────┘ └─────┘ └──────────────────────┘
src └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
typ └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
doc └────┘ └──────────┘ └┘ └─
txt └────┘ └──────────┘ └┘ └─
par └────┘ └──────────┘ └┘ └─
pid ┴┴ └──────────┘ └┘ ┴└
st └────────────────────────────────────────────────────────────────────────────────
534
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
535 @[simp] theorem lcm_self (i : ℤ) : lcm i i = nat_abs i :=
id ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴
src ┴ └─┘ ┴ └─────┘
typ ┴ └─┘ ┴ ┴ ┴ └─────┘ ┴
doc └──┘ └─┘
536 by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_lcm, coe_nat_abs_eq_normalize]
id └────────────────────────┘ └─────┘ └──────────────────────┘
src └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
typ └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
doc └────┘ └──────────┘ └┘ └─
txt └────┘ └──────────┘ └┘ └─
par └────┘ └──────────┘ └┘ └─
pid ┴┴ └──────────┘ └┘ ┴└
st └────────────────────────────────────────────────────────────────────────────────
537
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
538 theorem dvd_lcm_left (i j : ℤ) : i ∣ lcm i j :=
id ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ ┴ └─┘
typ ┴ ┴ ┴ └─┘ ┴ ┴
doc └─┘
539 by rw [coe_lcm]; exact dvd_lcm_left _ _
id └─────┘ └──────────┘
src └──┘└─────┘┴ └────┘└──────────┘└────
typ └──┘└─────┘┴ └────┘└──────────┘└────
doc └──┘ ┴ └────┘ └────
txt └──┘ ┴ └────┘ └────
par └──┘ ┴ └────┘ └────
pid └┘ ┴ ┴ └──┘└
st └──────────┘┴└────────────────────────
540
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
541 theorem dvd_lcm_right (i j : ℤ) : j ∣ lcm i j :=
id ┴ ┴ ┴ └─┘ ┴ ┴
src ┴ ┴ └─┘
typ ┴ ┴ ┴ └─┘ ┴ ┴
doc └─┘
542 by rw [coe_lcm]; exact dvd_lcm_right _ _
id └─────┘ └───────────┘
src └──┘└─────┘┴ └────┘└───────────┘└────
typ └──┘└─────┘┴ └────┘└───────────┘└────
doc └──┘ ┴ └────┘ └────
txt └──┘ ┴ └────┘ └────
par └──┘ ┴ └────┘ └────
pid └┘ ┴ ┴ └──┘└
st └──────────┘┴└─────────────────────────
543
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
544 theorem lcm_dvd {i j k : ℤ} : i ∣ k → j ∣ k → (lcm i j : ℤ) ∣ k :=
id ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
src ┴ ┴ ┴ └─┘ ┴ ┴
typ ┴ ┴ ┴ ┴ ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴ ┴
doc └─┘
545 by rw [coe_lcm]; exact lcm_dvd
id └─────┘ └─────┘
src └──┘└─────┘┴ └────┘└─────┘└
typ └──┘└─────┘┴ └────┘└─────┘└
doc └──┘ ┴ └────┘ └
txt └──┘ ┴ └────┘ └
par └──┘ ┴ └────┘ └
pid └┘ ┴ ┴ └
st └──────────┘┴└───────────────
546
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
547 end int
548
549 theorem irreducible_iff_nat_prime : ∀(a : ℕ), irreducible a ↔ nat.prime a
id ┴ ┴ └─────────┘ ┴ ┴ └───────┘ ┴
src ┴ └─────────┘ ┴ └───────┘
typ ┴ ┴ └─────────┘ ┴ ┴ └───────┘ ┴
doc └─────────┘ └───────┘
550 | 0 := by simp [nat.not_prime_zero]
id └────────────────┘
src └────┘└────────────────┘└┘
typ └────┘└────────────────┘└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └─────────────────────────┘
551 | 1 := by simp [nat.prime, one_lt_two]
id └───────┘ └────────┘
src └────┘└───────┘└┘└────────┘└┘
typ └────┘└───────┘└┘└────────┘└┘
doc └────┘└───────┘└┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st └────────────────────────────┘
552 | (n + 2) :=
id ┴ ┴
src ┴
typ ┴ ┴
553 have h₁ : ¬n + 2 = 1, from dec_trivial,
id ┴ ┴ ┴ └─────────┘
src ┴ ┴ ┴ └─────────┘
typ ┴ ┴ ┴ └─────────┘
doc └─────────┘
554 begin
st └─────
555 simp [h₁, nat.prime, irreducible, (≥), nat.le_add_left 2 n, (∣)],
id └┘ └───────┘ └─────────┘ ┴ └─────────────┘ ┴
src └────┘ └┘└───────┘└┘└─────────┘└┘┴└──┘└─────────────┘└─┘ └┘ └─┘
typ └────┘└┘└┘└───────┘└┘└─────────┘└┘┴└──┘└─────────────┘└─┘┴└┘ └─┘
doc └────┘ └┘└───────┘└┘└─────────┘└┘ └──┘ └─┘ └┘ └─┘
txt └────┘ └┘ └┘ └┘ └──┘ └─┘ └┘ └─┘
par └────┘ └┘ └┘ └┘ └──┘ └─┘ └┘ └─┘
pid ┴┴ └┘ └┘ └┘ └──┘ └─┘ └┘ └─┘
st ───────────────────────────────────────────────────────────────────┘└─
556 refine forall_congr (assume a, forall_congr $ assume b, forall_congr $ assume hab, _),
id └──────────┘
src └─────┘ ┴ └──┘ ┴ ┴ └──┘└──────────┘┴ ┴ └──────┘
typ └─────┘ ┴ └──┘ ┴ ┴ └──┘└──────────┘┴ ┴ └──────┘
doc └─────┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └──────┘
txt └─────┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └──────┘
par └─────┘ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └──────┘
pid ┴ ┴ └──┘ ┴ ┴ └──┘ ┴ ┴ └──────┘
st ────────────────────────────────────────────────────────────────────────────────────────┘└─
557 by_cases a = 1; simp [h],
id ┴ ┴ ┴
src └───────┘ ┴┴└┘ └────┘ ┴
typ └───────┘┴┴┴└┘ └────┘┴┴
doc └───────┘ ┴ └┘ └────┘ ┴
txt └───────┘ ┴ └┘ └────┘ ┴
par └───────┘ ┴ └┘ └────┘ ┴
pid ┴ ┴ ┴┴ ┴┴ ┴
st ───────────────────────────┘└─
558 split,
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
st ────────┘└─
559 { assume hb, simpa [hb] using hab.symm },
id └┘ └──────┘
src └───────┘ └─────┘ └──────┘└──────┘┴
typ └───────┘ └─────┘└┘└──────┘└──────┘┴
doc └───────┘ └─────┘ └──────┘ ┴
txt └───────┘ └─────┘ └──────┘ ┴
par └───────┘ └─────┘ └──────┘ ┴
pid └───────┘ ┴┴ ┴┴└────┘ ┴
st ─────┘└───────┘└──────────────────────────┘└┘└
560 { assume ha, subst ha,
id └┘
src └───────┘ └────┘
typ └───────┘ └────┘└┘
doc └───────┘ └────┘
txt └───────┘ └────┘
par └───────┘ └────┘
pid └───────┘ ┴
st ──────────────┘└────────┘└─
561 have : n + 2 > 0, from dec_trivial,
id ┴ ┴ ┴ └─────────┘
src └─────┘ ┴┴└─┘┴└┘ └───┘└─────────┘
typ └─────┘┴┴┴└─┘┴└┘ └───┘└─────────┘
doc └─────┘ ┴ └─┘ └┘ └───┘
txt └─────┘ ┴ └─┘ └┘ └───┘
par └─────┘ ┴ └─┘ └┘ └───┘
pid └───┘└┘ ┴ └─┘ ┴┴ └───┘
st ─────────────────────┘└────────────────┘└─
562 refine nat.eq_of_mul_eq_mul_left this _,
id └───────────────────────┘ └──┘
src └─────┘└───────────────────────┘┴ └┘
typ └─────┘└───────────────────────┘┴└──┘└┘
doc └─────┘ ┴ └┘
txt └─────┘ ┴ └┘
par └─────┘ ┴ └┘
pid ┴ ┴ └┘
st ────────────────────────────────────────────┘└─
563 rw [← hab, mul_one] }
id └─┘ └─────┘
src └────┘ └┘└─────┘└┘
typ └────┘└─┘└┘└─────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid └──┘ └┘ ┴┴
st ──────────────┘└───────┘┴┴└─
564 end
st ────┘
565
566 lemma nat.prime_iff_prime {p : ℕ} : p.prime ↔ _root_.prime (p : ℕ) :=
id ┴ ┴└────┘ ┴ └──────────┘ ┴ ┴
src ┴ └────┘ ┴ └──────────┘ ┴
typ ┴ ┴└────┘ ┴ └──────────┘ ┴ ┴
doc └────┘ └──────────┘
567 ⟨λ hp, ⟨nat.pos_iff_ne_zero.1 hp.pos, mt is_unit_iff_dvd_one.1 hp.not_dvd_one,
id └┘ └─────────────────┘┴ └┘└──┘ └┘ └─────────────────┘┴ └┘└──────────┘
src └─────────────────┘┴ └──┘ └┘ └─────────────────┘┴ └──────────┘
typ └┘ └─────────────────┘┴ └┘└──┘ └┘ └─────────────────┘┴ └┘└──────────┘
568 λ a b, hp.dvd_mul.1⟩,
id ┴ ┴ └┘└──────┘┴
src └──────┘┴
typ ┴ ┴ └┘└──────┘┴
569 λ hp, ⟨nat.one_lt_iff_ne_zero_and_ne_one.2 ⟨hp.1, λ h1, hp.2.1 $ h1.symm ▸ is_unit_one⟩,
id └┘ └───────────────────────────────┘┴ └┘┴ └┘ └┘┴ ┴ └┘└───┘ ┴ └─────────┘
src └───────────────────────────────┘┴ ┴ ┴ ┴ └───┘ ┴ └─────────┘
typ └┘ └───────────────────────────────┘┴ └┘┴ └┘ └┘┴ ┴ └┘└───┘ ┴ └─────────┘
570 λ a h, let ⟨b, hab⟩ := h in
id ┴ ┴ └─┘ ┴ └─┘ ┴
typ ┴ ┴ └─┘ ┴ └─┘ ┴
571 (hp.2.2 a b (hab ▸ dvd_refl _)).elim
id └┘┴ ┴ ┴ ┴ └──────┘ └──┘
src ┴ ┴ ┴ └──────┘ └──┘
typ └┘┴ ┴ ┴ ┴ └──────┘ └──┘
572 (λ ha, or.inr (nat.dvd_antisymm h ha))
id └┘ └────┘ └──────────────┘ ┴ └┘
src └────┘ └──────────────┘
typ └┘ └────┘ └──────────────┘ ┴ └┘
573 (λ hb, or.inl (have hpb : p = b, from nat.dvd_antisymm hb
id └┘ └────┘ ┴ ┴ └──────────────┘ └┘
src └────┘ ┴ └──────────────┘
typ └┘ └────┘ ┴ ┴ └──────────────┘ └┘
574 (hab.symm ▸ dvd_mul_left _ _),
id └───┘ ┴ └──────────┘
src └───┘ ┴ └──────────┘
typ └───┘ ┴ └──────────┘
575 (nat.mul_left_inj (show 0 < p, from
id └──────────────┘ ┴ ┴
src └──────────────┘ ┴
typ └──────────────┘ ┴ ┴
576 nat.pos_of_ne_zero hp.1)).1 $
id └────────────────┘ └┘┴ ┴
src └────────────────┘ ┴ ┴
typ └────────────────┘ └┘┴ ┴
577 by rw [hpb, mul_comm, ← hab, hpb, mul_one]))⟩⟩
id └─┘ └──────┘ └─┘ └─┘ └─────┘
src └──┘ └┘└──────┘└──┘ └┘ └┘└─────┘┴
typ └──┘└─┘└┘└──────┘└──┘└─┘└┘└─┘└┘└─────┘┴
doc └──┘ └┘ └──┘ └┘ └┘ ┴
txt └──┘ └┘ └──┘ └┘ └┘ ┴
par └──┘ └┘ └──┘ └┘ └┘ ┴
pid └┘ └┘ └──┘ └┘ └┘ ┴
st └──────┘└────────┘└─────┘└───┘└───────┘┴
578
579 lemma nat.prime_iff_prime_int {p : ℕ} : p.prime ↔ _root_.prime (p : ℤ) :=
id ┴ ┴└────┘ ┴ └──────────┘ ┴ ┴
src ┴ └────┘ ┴ └──────────┘ ┴
typ ┴ ┴└────┘ ┴ └──────────┘ ┴ ┴
doc └────┘ └──────────┘
580 ⟨λ hp, ⟨int.coe_nat_ne_zero_iff_pos.2 hp.pos, mt is_unit_int.1 hp.ne_one,
id └┘ └─────────────────────────┘┴ └┘└──┘ └┘ └─────────┘┴ └┘└─────┘
src └─────────────────────────┘┴ └──┘ └┘ └─────────┘┴ └─────┘
typ └┘ └─────────────────────────┘┴ └┘└──┘ └┘ └─────────┘┴ └┘└─────┘
581 λ a b h, by rw [← int.dvd_nat_abs, int.coe_nat_dvd, int.nat_abs_mul, hp.dvd_mul] at h;
id ┴ ┴ ┴ └─────────────┘ └─────────────┘ └─────────────┘
src └────┘└─────────────┘└┘└─────────────┘└┘└─────────────┘└┘ └────┘
typ ┴ ┴ ┴ └────┘└─────────────┘└┘└─────────────┘└┘└─────────────┘└┘└────────┘└────┘
doc └────┘ └┘ └┘ └┘ └────┘
txt └────┘ └┘ └┘ └┘ └────┘
par └────┘ └┘ └┘ └┘ └────┘
pid └──┘ └┘ └┘ └┘ ┴└───┘
st └────────────────────┘└───────────────┘└───────────────┘└──────────┘┴└──────
582 rwa [← int.dvd_nat_abs, int.coe_nat_dvd, ← int.dvd_nat_abs, int.coe_nat_dvd]⟩,
id └─────────────┘ └─────────────┘ └─────────────┘ └─────────────┘
src └─────┘└─────────────┘└┘└─────────────┘└──┘└─────────────┘└┘└─────────────┘┴
typ └─────┘└─────────────┘└┘└─────────────┘└──┘└─────────────┘└┘└─────────────┘┴
doc └─────┘ └┘ └──┘ └┘ ┴
txt └─────┘ └┘ └──┘ └┘ ┴
par └─────┘ └┘ └──┘ └┘ ┴
pid └──┘ └┘ └──┘ └┘ ┴
st ────────┘└───────────────┘└───────────────┘└─────────────────┘└───────────────┘┴
583 λ hp, nat.prime_iff_prime.2 ⟨int.coe_nat_ne_zero.1 hp.1,
id └┘ └─────────────────┘┴ └─────────────────┘┴ └┘┴
src └─────────────────┘┴ └─────────────────┘┴ ┴
typ └┘ └─────────────────┘┴ └─────────────────┘┴ └┘┴
584 mt is_unit_nat.1 $ λ h, by simpa [h, not_prime_one] using hp,
id └┘ └─────────┘┴ ┴ ┴ └───────────┘ └┘
src └┘ └─────────┘┴ └─────┘ └┘└───────────┘└──────┘
typ └┘ └─────────┘┴ ┴ └─────┘┴└┘└───────────┘└──────┘└┘
doc └─────┘ └┘ └──────┘
txt └─────┘ └┘ └──────┘
par └─────┘ └┘ └──────┘
pid ┴┴ └┘ ┴┴└────┘
st └────────────────────────────────┘
585 λ a b, by simpa only [int.coe_nat_dvd, (int.coe_nat_mul _ _).symm] using hp.2.2 a b⟩⟩
id ┴ ┴ └─────────────┘ └─────────────┘ └┘ ┴ ┴
src └──────────┘└─────────────┘└┘ └─────────────┘└────────────────┘ └───┘ ┴
typ ┴ ┴ └──────────┘└─────────────┘└┘ └─────────────┘└────────────────┘└┘└───┘┴┴┴
doc └──────────┘ └┘ └────────────────┘ └───┘ ┴
txt └──────────┘ └┘ └────────────────┘ └───┘ ┴
par └──────────┘ └┘ └────────────────┘ └───┘ ┴
pid ┴└──┘└┘ └┘ └─────────┘┴└────┘ └───┘ ┴
st └────────────────────────────────────────────────────────────────────────┘
586
587 def associates_int_equiv_nat : associates ℤ ≃ ℕ :=
id └────────┘ ┴ ┴ ┴
src └────────┘ ┴ ┴ ┴
typ └────────┘ ┴ ┴ ┴
doc ┴
588 begin
st └─────
589 refine ⟨λz, z.out.nat_abs, λn, associates.mk n, _, _⟩,
id └──┘└──────┘ └───────────┘
src └─────┘ └─┘ └──┘└──────┘└┘ └─┘└───────────┘┴ └─────┘
typ └─────┘ └─┘ └──┘└──────┘└┘ └─┘└───────────┘┴ └─────┘
doc └─────┘ └─┘ └┘ └─┘ ┴ └─────┘
txt └─────┘ └─┘ └┘ └─┘ ┴ └─────┘
par └─────┘ └─┘ └┘ └─┘ ┴ └─────┘
pid ┴ └─┘ └┘ └─┘ ┴ └─────┘
st ──────────────────────────────────────────────────────┘└─
590 { refine (assume a, quotient.induction_on' a $ assume a,
id └────────────────────┘
src └─────┘ └──┘└────────────────────┘┴ ┴ ┴ └───
typ └─────┘ └──┘└────────────────────┘┴ ┴ ┴ └───
doc └─────┘ └──┘ ┴ ┴ ┴ └───
txt └─────┘ └──┘ ┴ ┴ ┴ └───
par └─────┘ └──┘ ┴ ┴ ┴ └───
pid ┴ └──┘ ┴ ┴ ┴ └───
st ───┘└──────────────────────────────────────────────────────
591 associates.mk_eq_mk_iff_associated.2 $ associated.symm $ ⟨norm_unit a, _⟩),
id └────────────────────────────────┘ └─────────────┘ └───────┘
src ─────┘└────────────────────────────────┘└─┘ ┴└─────────────┘┴ ┴ └───────┘┴ └───┘
typ ─────┘└────────────────────────────────┘└─┘ ┴└─────────────┘┴ ┴ └───────┘┴ └───┘
doc ─────┘ └─┘ ┴ ┴ ┴ ┴ └───┘
txt ─────┘ └─┘ ┴ ┴ ┴ ┴ └───┘
par ─────┘ └─┘ ┴ ┴ ┴ ┴ └───┘
pid ─────┘ └─┘ ┴ ┴ ┴ ┴ └───┘
st ───────────────────────────────────────────────────────────────────────────────┘└─
592 show normalize a = int.nat_abs (normalize a),
id ┴ └─────────┘ └───────┘ ┴
src └───┘ ┴ ┴┴┴└─────────┘┴ └───────┘┴ ┴
typ └───┘ ┴ ┴┴┴└─────────┘┴ └───────┘┴┴┴
doc └───┘ ┴ ┴ ┴ ┴ ┴ ┴
txt └───┘ ┴ ┴ ┴ ┴ ┴ ┴
par └───┘ ┴ ┴ ┴ ┴ ┴ ┴
pid └───┘ ┴ ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────────┘└─
593 rw [int.coe_nat_abs_eq_normalize, normalize_idem] },
id └──────────────────────────┘ └────────────┘
src └──┘└──────────────────────────┘└┘└────────────┘└┘
typ └──┘└──────────────────────────┘└┘└────────────┘└┘
doc └──┘ └┘ └┘
txt └──┘ └┘ └┘
par └──┘ └┘ └┘
pid └┘ └┘ ┴┴
st ───────────────────────────────────┘└──────────────┘┴┴└┘└
594 { assume n, show int.nat_abs (normalize n) = n,
id └─────────┘ └───────┘ ┴
src └──────┘ └───┘└─────────┘┴ └───────┘┴ └┘ ┴
typ └──────┘ └───┘└─────────┘┴ └───────┘┴ └┘ ┴┴
doc └──────┘ └───┘ ┴ ┴ └┘ ┴
txt └──────┘ └───┘ ┴ ┴ └┘ ┴
par └──────┘ └───┘ ┴ ┴ └┘ ┴
pid └──────┘ └───┘ ┴ ┴ └┘ ┴
st ───────────┘└──────────────────────────────────┘└─
595 rw [← int.coe_nat_abs_eq_normalize, int.nat_abs_of_nat, int.nat_abs_of_nat] }
id └──────────────────────────┘ └────────────────┘ └────────────────┘
src └────┘└──────────────────────────┘└┘└────────────────┘└┘└────────────────┘└┘
typ └────┘└──────────────────────────┘└┘└────────────────┘└┘└────────────────┘└┘
doc └────┘ └┘ └┘ └┘
txt └────┘ └┘ └┘ └┘
par └────┘ └┘ └┘ └┘
pid └──┘ └┘ └┘ ┴┴
st ─────────────────────────────────────┘└──────────────────┘└──────────────────┘┴┴└─
596 end
st ──┘